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:
-
498
Packages
-
10
New packages this month
-
17
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-hierarchy-builder
Compatibility package for rocq-hierarchy-builder
coq-ext-lib
A library of Coq definitions, theorems, and tactics
New Packages
rocq-hierarchy-builder
High level commands to declare and evolve a hierarchy based on packed classes
rocq-mathcomp-finmap
Finite sets, finite maps, finitely supported functions
rocq-verified-extraction
Verified extraction from Rocq to OCaml
rocq-autosubst-ocaml
OCaml implementation of Autosubst for Rocq
rocq-mathcomp-algebra
Mathematical Components Library on Algebra
Recently Updated
coq-graph-theory-planar
Graph theory results on planarity in Coq and MathComp
coq-graph-theory
General graph theory definitions and results in Coq and MathComp
coq-mathcomp-multinomials
A Multivariate polynomial Library for the Mathematical Components Library
coq-mathcomp-odd-order
The formal proof of the Feit-Thompson theorem
coq-mathcomp-real-closed
Mathematical Components Library on real closed fields
community
Start Contributing
Learn how to publish your first Rocq opam package today and make it available to the rest of the community.
