MetaCoq 1.2.1 for Coq 8.18

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