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:
-
510
Packages
-
12
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-hierarchy-builder
Compatibility package for rocq-hierarchy-builder
coq-ext-lib
A library of Coq definitions, theorems, and tactics
New Packages
coq-trocq-hott-examples
A modular parametricity plugin for proof transfer in Coq: examples
coq-trocq-hott
A modular parametricity plugin for proof transfer in Coq
coq-trocq-std-examples
A modular parametricity plugin for proof transfer in Coq: examples
coq-trocq-std
A modular parametricity plugin for proof transfer in Coq
rocq-parseque
Total parser combinators in Rocq/Coq
Recently Updated
coq-hol-light-real-with-N
Definition of HOL-Light real numbers in Coq using N
coq-elpi
Compatibility metapackage for Elpi extension language after the Rocq renaming
rocq-elpi
Elpi extension language for Coq
coq-infotheo
Discrete probabilities and information theory 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.
