MetaCoq 1.2.1 for Coq 8.17

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
• 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
• Add a merge operation for the global env by @JasonGross in #955
• improve strengthening to get cumul info on type by @tabareau in #985
• remove parameters in firstorder inductive types by @tabareau in #986
• 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
• Merge 8.16 into 8.17 by @yforster in #992
• use names in EAst.t by @tabareau in #997
• Add a let in front of case in implement_box by @yforster in #999
• Qualify imports to disable race condition for opam builds by @yforster in #1001

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