We are pleased to announce the release of MetaRocq 1.5.1 for Rocq 9.1. This version includes a new (unsafe/unverified) phase for remapping inductive types and their pattern-matching constructs to arbitrary constants in the erasure pipeline (e.g. to map nat to zarith/GMP in backends). The library now depends on coq-ext-lib for its monad library and includes a few bug fixes.
What's Changed
- Add workspace info for vscode to Install by @thomas-lamiaux in #1176
- Fix outdated version numbers in the documentation by @jrosain in #1181
- Fix handling of fresh_universes after tmMkInductive by restarting fro… by @mattam82 in #1188
- map_constr_with_binders by @BasileGros in #1187
- Backport of "Don't overwrite COQEXTRAFLAGS in test suite" by @yforster in #1203
- New unsafe pass to extract inductives to arbitrary constants by @mattam82 in #1238
- Remap not just one inductive but whole blocks at a time. by @mattam82 in #1239
- Adapt map_term_with_context for 9.1 guard condition by @BasileGros in #1234
- Fix remapping phase by @mattam82 in #1243
- Update 9.1 from 9.0 by @mattam82 in #1245
- Merge 9.0 changes in 9.1 by @mattam82 in #1244
- [experiment] Use ext-lib monads by @4ever2 in #1241
- Fix opaque access, using a custom coqpp state specifier by @mattam82 in #1247
- doc: Add missing step to include Rocq repo when building from source by @TDiazT in #1236
- Bump actions/checkout from 4 to 6 by @dependabot[bot] in #1210
- Fix template pluging mlpack by @mattam82 in #1248
New Contributors
- @BasileGros made their first contribution in #1187
Full Changelog: v1.4.1-9.1...v1.5.1-9.1