Highlights

• 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

Changes

See the full changelog in the reference manual.

Installation Instructions

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

opam update
opam switch create 4.14.1
opam pin add rocq-runtime 9.1.0
opam install rocq-prover

Refer to the general install instructions for more information.

Source Distribution

• Source tarball (.tar.gz) for compilation under Unix (including Linux and macOS X) and Microsoft Windows (including Cygwin).
• Opam is a source-based distribution of OCaml, Rocq and many companion libraries and tools. Compilation and installation are automated by powerful package managers.
• The official development repo is hosted on GitHub.