Skip to content

MetaRocq 1.4 for Rocq 9.0

Choose a tag to compare

View all tags
@mattam82 mattam82 released this 26 Mar 10:48
v1.4-9.0
ac5651a
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

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
    • Improve evar handling in tmUnquote (#1113)
    • tmMkInductive should not be used in a tactic (#1130)
    • Remove lambda and letin cumulativity (#1151)

Full Changelog: v1.3.4-9.0...v1.4-9.0

Contributors

mattam82
Assets 3
Loading