The 9.0.1 version contains a few fixes due to corrections in the guard checker of Rocq. This release implements the renaming from Coq to Rocq, MetaCoq to MetaRocq and TemplateCoq to TemplateRocq.
As such, it is incompatible with previous releases. From the user point of view, you will need to adapt your Require Imports from From MetaCoq. to From MetaRocq. and a few utility modules (in MetaRocq.utils) changed names from MC to MR, e.g. MCList becomes MRList, which will affect qualified references to these modules. The commands MetaCoq Run, SafeCheck etc... have also been renamed.
What's Changed
- Coq -> Rocq, MetaCoq -> MetaRocq, TemplateCoq -> TemplateRocq renaming by @mattam82 in #1153
- Cherry picks on 9.0 by @mattam82 in #1154
- Fix the proof using a hole in the guard checker by @yannl35133 in #1160
- Take relevance into account for typing by @yannl35133 in #1163
- Nix CI for Rocq-9.0 by @4ever2 in #1164
- 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 @DeLectionnes in #1187
- Backport of "Don't overwrite COQEXTRAFLAGS in test suite" by @yforster in #1203
New Contributors
- @thomas-lamiaux made their first contribution in #1176
- @DeLectionnes made their first contribution in #1187
Full Changelog: v1.4-9.0...v1.4-9.0.1