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:
-
518
Packages
-
2
New packages this month
-
6
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-libhyps
Hypotheses manipulation library
rocq-mathcomp-hollight-real-with-N
HOL-Light definition of real numbers in Rocq using N and MathComp
Recently Updated
coq-rupicola
Gallina to imperative code compilation, currently in design phase
coq-bedrock2
A work-in-progress language and compiler for verified low-level programming
coq-coqutil
Coq library for tactics, basic definitions, sets, maps
coq-hammer-tactics
Reconstruction tactics for the hammer for Coq
coq-hammer
General-purpose automated reasoning hammer tool for Coq
community
Start Contributing
Learn how to publish your first Rocq opam package today and make it available to the rest of the community.
