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
extendsby @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_boxby @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