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:
-
564
Packages
-
27
New packages this month
-
46
Updates this week
packages
Most Used
coq-mathcomp-ssreflect
Compatibility package for rocq-mathcomp-ssreflect
rocq-stdlib
The Rocq Proof Assistant -- Standard Library
coq-mathcomp-algebra
Compatibility package for rocq-mathcomp-algebra
coq-flocq
A formalization of floating-point arithmetic for the Coq system
coq-hierarchy-builder
Compatibility package for rocq-hierarchy-builder
New Packages
rocq-mathcomp-analysis-stdlib
A library to link real numbers from mathematical components and Stdlib
rocq-mathcomp-analysis
An analysis library for mathematical components
rocq-mathcomp-classical
A library for classical logic for mathematical components
rocq-mathcomp-experimental-reals
A library for alternative real numbers for mathematical components
rocq-mathcomp-reals-stdlib
A library to link real numbers from mathematical components and Stdlib
Recently Updated
coq-mathcomp-analysis-stdlib
Compatibility package for rocq-mathcomp-analysis-stdlib
coq-mathcomp-analysis
Compatibility package for rocq-mathcomp-analysis
coq-mathcomp-classical
Compatibility package for rocq-mathcomp-classical
coq-mathcomp-experimental-reals
Compatibility package for rocq-mathcomp-experimental-reals
coq-mathcomp-reals-stdlib
Compatibility package for rocq-mathcomp-reals-stdlib
community
Start Contributing
Learn how to publish your first Rocq opam package today and make it available to the rest of the community.
