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:
-
529
Packages
-
10
New packages this month
-
38
Updates this week
packages
Most Used
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
coq-hierarchy-builder
Compatibility package for rocq-hierarchy-builder
New Packages
coq-mathcomp-boot
Compatibility package for rocq-mathcomp-boot
coq-mathcomp-order
Compatibility package for rocq-mathcomp-order
rocq-mathcomp-boot
Small Scale Reflection
rocq-mathcomp-order
Mathematical Components Library on order theory
rocq-color
A library on rewriting theory and termination
Recently Updated
coq-fourcolor-reals
Interface for real numbers used in the Four Color Theorem
coq-fourcolor
Mechanization of the Four Color Theorem in Coq
coq-graph-theory
General graph theory definitions and results in Coq and MathComp
coq-libvalidsdp
LibValidSDP
coq-mathcomp-algebra
Compatibility package for rocq-mathcomp-algebra
community
Start Contributing
Learn how to publish your first Rocq opam package today and make it available to the rest of the community.
