MetaRocq/metarocq v1.4-9.0

MetaRocq 1.4 for Rocq 9.0

on GitHub

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