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:
-
567
Packages
-
3
New packages this month
-
10
Updates this week
packages
Most Used
coq-mathcomp-ssreflect
Compatibility package for rocq-mathcomp-ssreflect
rocq-stdlib
The Rocq Proof Assistant -- Standard Library
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
New Packages
rocq-listz
A Rocq library of lists with indices in Z
rocq-micromega-plugin
Micromega plugin for Rocq
rocq-certirocq
A Verified Compiler for Gallina, Written in Gallina
Recently Updated
rocq-listz
A Rocq library of lists with indices in Z
rocq-libhyps
Hypotheses manipulation library
rocq-micromega-plugin
Micromega plugin for Rocq
coq-kruskal-almostfull
Base Coq library for manipulating Almost Full relations
coq-kruskal-fan
Extending Coq library for manipulating Almost Full relations with the FAN theorem
community
Start Contributing
Learn how to publish your first Rocq opam package today and make it available to the rest of the community.
