Rocq Packages
Explore hundreds of Rocq packages with their documentation
Install Rocq Packages
Publish a Rocq Package
opam
Package Manager for OCaml and Rocq
The source-based package manager opam supports OCaml and Rocq packages. With opam installed, released Rocq packages can be accessed by adding the official Rocq opam repository:
-
598
Packages
-
6
New packages this month
-
10
Updates this week
packages
Most Used
rocq-stdlib
The Rocq Proof Assistant -- Standard Library
coq-mathcomp-ssreflect
Compatibility package for rocq-mathcomp-ssreflect
coq-mathcomp-algebra
Compatibility package for rocq-mathcomp-algebra
coq-flocq
A formalization of floating-point arithmetic for the Coq system
coq-ext-lib
A library of Coq definitions, theorems, and tactics
New Packages
rocq-mltac2
Ltac2 APIs in OCaml
ppx_rocq
PPX syntax extensions for quoting Rocq terms in OCaml
rocq-pi-leibniz
Constructive pi for the Rocq constructive Cauchy reals with premise-free rational separation
rocq-partial
A Rocq library for extractable partial functions
rocq-actris
A framework for session protocol reasoning in Iris
Recently Updated
rocq-formalv-check_range
Tactics to automatically prove Boolean goals involving Uint63/Sint63 variables
rocq-formalv-prim63_mathcomp
Refinements from MathComp nat and int to Rocq primitive integers Uint63/Sint63
rocq-formalv-time
A Rocq library for time and date arithmetic according to the UTC standard with leap seconds
rocq-read-file
Read files from disk into Rocq primitive values
rocq-mltac2
Ltac2 APIs in OCaml
community
Start Contributing
Learn how to publish your first Rocq opam package today and make it available to the rest of the community.
