MetaRocq 1.5.1 for Rocq 9.1

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