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
Full Changelog: v1.2-8.17...v1.2.1-8.18