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 https://github.com/MetaCoq/metacoq/pull/953 Add boolean versions of the varieties of extends by @JasonGross in https://github.com/MetaCoq/metacoq/pull/954 Add union and inter checker flags by @JasonGross in https://github.com/MetaCoq/metacoq/pull/957 Add MCListable class for enumerating finite types by @JasonGross in https://github.com/MetaCoq/metacoq/pull/962 Close computational obligations with defined in erase_global_decls by @yforster in https://github.com/MetaCoq/metacoq/pull/961 Invariants in named recursion rule by @yforster in https://github.com/MetaCoq/metacoq/pull/967 Add a merge operation for the global env by @JasonGross in https://github.com/MetaCoq/metacoq/pull/955 improve strengthening to get cumul info on type by @tabareau in https://github.com/MetaCoq/metacoq/pull/985 remove parameters in firstorder inductive types by @tabareau in https://github.com/MetaCoq/metacoq/pull/986 Drastically speed up ByteCompareSpec by @JasonGross in https://github.com/MetaCoq/metacoq/pull/988 Verified erasure pipeline by @mattam82 in https://github.com/MetaCoq/metacoq/pull/987 add not_isErasable lemma in EArities by @tabareau in https://github.com/MetaCoq/metacoq/pull/990 Merge 8.16 into 8.17 by @yforster in https://github.com/MetaCoq/metacoq/pull/992 use names in EAst.t by @tabareau in https://github.com/MetaCoq/metacoq/pull/997 Add a let in front of case in implement_box by @yforster in https://github.com/MetaCoq/metacoq/pull/999 Qualify imports to disable race condition for opam builds by @yforster in https://github.com/MetaCoq/metacoq/pull/1001 Full Changelog: https://github.com/MetaCoq/metacoq/compare/v1.2-8.17...v1.2.1-8.17