MetaRocq/metarocq v1.2.1-8.18 on GitHub

This is a minor release synchronising the state of coq-8.17 and coq-8.18 to allow publishing an opam package for Coq 8.18. See https://github.com/MetaCoq/metacoq/releases/tag/v1.2-8.17 for detailed release notes.

What's Changed

Fix monad_map_branches_k name by @JasonGross in #953
Add boolean versions of the varieties of extends by @JasonGross in #954
Add union and inter checker flags by @JasonGross in #957
Adapt w.r.t. coq/coq#17564. by @ppedrot in #960
Add MCListable class for enumerating finite types by @JasonGross in #962
Close computational obligations with defined in erase_global_decls by @yforster in #961
Invariants in named recursion rule by @yforster in #967
Drastically speed up ByteCompareSpec by @JasonGross in #988
Verified erasure pipeline by @mattam82 in #987
add not_isErasable lemma in EArities by @tabareau in #990
Add quotation API for context and global_env_ext by @JasonGross in #996

Additionally, the following adaptions were necessary to work with Coq 8.18:

Show

Update coq 8.18 with commits from 8.17 by @yforster in #1000
Update 8.18 again with Makefile and opam change by @yforster in #1003
Merge 8.16 and 8.17 into 8.18 by @yforster in #991
Adapt to coq/coq#16890 (Classes.existing_instance takes globref not qualid) by @SkySkimmer in #959
Remove bugkncst by @SkySkimmer in #963
Adapt to coq/coq#17633 (decompose_app returns array not list) by @SkySkimmer in #965
Adapt to coq/coq#17585 (revised warning API) by @SkySkimmer in #964
Adapt to coq/coq#17664 (goptions use Deprecation.t option instead of bool) by @SkySkimmer in #968
Bump cachix/install-nix-action from 20 to 21 by @dependabot in #966
Add a merge operation for the global env by @JasonGross in #955
Use : Set explicitly when needed by @SkySkimmer in #971
Bump cachix/install-nix-action from 21 to 22 by @dependabot in #970
Bump cachix/install-nix-action from 21 to 22 by @dependabot in #973
Bump cachix/install-nix-action from 20 to 22 by @dependabot in #974
Adapt w.r.t. coq/coq#17781. by @ppedrot in #972
Adapt to coq PR #17991 which lets "simpl" refolds partial applications of fixpoints by @herbelin in #975
Bump actions/checkout from 3 to 4 by @dependabot in #978
Bump actions/checkout from 3 to 4 by @dependabot in #977
Bump cachix/install-nix-action from 22 to 23 by @dependabot in #979
Bump actions/checkout from 3 to 4 by @dependabot in #982
improve strengthening to get cumul info on type by @tabareau in #985
remove parameters in firstorder inductive types by @tabareau in #986
Remove Int31 by @Villetaneuse in #983
Adapt w.r.t. coq/coq#16004. by @ppedrot in #721
Adapt w.r.t. coq/coq#16004. by @ppedrot in #724
prepare for coq/coq#16289 by @mrhaandi in #734
improved auto goal selection by @mrhaandi in #737
Adapt w.r.t. coq/coq#16442. by @ppedrot in #755
Master cherry picks by @mattam82 in #759
Adapt w.r.t. coq/coq#16933. by @ppedrot in #797
Adapt w.r.t. coq/coq#16904. by @ppedrot in #798
Adapt to coq/coq#16938 (staged options) by @SkySkimmer in #804
Don't force references at linking time by @SkySkimmer in #809
Adapt w.r.t. coq/coq#16903. by @ppedrot in #806
Adapt w.r.t. coq/coq#17049. by @ppedrot in #824
Adapt w.r.t. coq/coq#17091. by @ppedrot in #827
Adapt w.r.t coq/coq#17021 by @andres-erbsen in #823
Adapt to coq/coq#17220 (genargs are not holes) by @SkySkimmer in #835
Adapt to coq/coq#17283 (more careful handling of univ mono term constructors) by @SkySkimmer in #861
Adapt to coq/coq#17331 by @maximedenes in #895
Adapt to coq/coq#17293 (wit_red_expr moved) by @SkySkimmer in #860

Full Changelog: v1.2-8.17...v1.2.1-8.18

MetaRocq/metarocq v1.2.1-8.18 MetaCoq 1.2.1 for Coq 8.18 on GitHub

What's Changed

MetaRocq/metarocq v1.2.1-8.18
MetaCoq 1.2.1 for Coq 8.18

on GitHub