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:
-
575
Packages
-
7
New packages this month
-
4
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
rocq-elpi-xml
Xml-light bindings for rocq-elpi
rocq-read-file
Read files from disk into Rocq primitive values
strict-order-solver
Complete solver for strict orders (transitive+irreflexive relations) for Rocq
rocq-laproof
LAProof: a library of formal proofs of accuracy and correctness for linear algebra programs
rocq-categories
A library for category theory
Recently Updated
coq-gappa
A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover
rocq-micromega-plugin
Micromega plugin for Rocq
coq-quickchick
Randomized Property-Based Testing for Coq
rocq-lean-import
Plugin allowing Rocq to import Lean exported files
community
Start Contributing
Learn how to publish your first Rocq opam package today and make it available to the rest of the community.
