Rocq Packages
Explore hundreds of open-source Rocq packages with their documentation
Publish a Package
opam
The OCaml and Rocq Package Manager
Opam is a source-based package manager for OCaml and Rocq. It supports multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow
-
514
Packages
-
2
New packages this month
-
10
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-equations
Compatibility package, see rocq-equations
New Packages
rocq-smpl
Smpl: An Extensible Tactic for Coq
coq-lean-import
Plugin allowing Coq to import Lean exported files
Recently Updated
coq-hierarchy-builder
Compatibility package for rocq-hierarchy-builder
rocq-hierarchy-builder
High level commands to declare and evolve a hierarchy based on packed classes
coq-compcert
The CompCert C compiler (64 bit)
coq-record-update
Generic support for updating record fields in Coq
coq-mathcomp-algebra-tactics
Ring, field, lra, nra, and psatz tactics for Mathematical Components
community
Start Contributing
Learn how to publish your first Opam package today and make it available to the rest of the community.
