View all changes

Release of Rocq 9.1.1

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

  • Fixed an anomaly when defining a sort polymorphic inductive without enabling Universe Polymorphism.
  • Fixed compatibility with OCaml 5.4 with warnings as errors

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 rocq-core=9.1.1

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