View all changes

Release of Rocq 9.1

We have the pleasure of announcing the first release of Rocq 9.1. The main changes are:

  • Fixed incorrect guard checking leading to inconsistencies
  • Sort polymorphic universe instances should now be written as @{s ; u} instead of @{s | u}
  • Fixed handling of notation variables for ltac2 in notations (i.e. Notation "'foo' x" := ltac2:(...))
  • Support for refine attribute in Definition
  • Rocq can be compile-time configured to be relocatable
  • Extraction handles sort polymorphic definitions

The full list of changes is available here for more details.

Installation Instructions

The base compiler can be installed as an opam switch with the following commands:

opam update
opam switch create 4.14.1
opam install rocq-prover.9.1.0

The source code for the release is also directly available on: