All Releases

Rocq Prover 9.1.1

This page describes The Rocq Prover version 9.1.1, released on February 2nd, 2026. Go here for a list of all releases.

This is the second release of The Rocq Prover, version 9, patch level 1.

Github release

Reference Manual

Corelib Theories

OCaml API

Stdlib Manual

Stdlib Theories

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
  • Fixed an anomaly when defining a sort polymorphic inductive without enabling Universe Polymorphism.
  • Fixed compatibility with OCaml 5.4 with warnings as errors

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.2
opam install rocq-prover rocq-core=9.1.1

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.