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:
-
582
Packages
-
7
New packages this month
-
42
Updates this week
packages
Most Used
coq-mathcomp-algebra
Compatibility package for rocq-mathcomp-algebra
coq-mathcomp-ssreflect
Compatibility package for rocq-mathcomp-ssreflect
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-mathcomp-multinomials
A Multivariate polynomial Library for the Mathematical Components Library
rocq-mathcomp-real-closed
Mathematical Components Library on real closed fields
rocq-mathcomp-finite-group
Mathematical Components Library on finite groups
rocq-mathcomp-group-representation
Mathematical Components Library on group representation theory
rocq-vst-ora
Ordered Resource Algebras for Iris
Recently Updated
rocq-micromega-plugin
Micromega plugin for Rocq
coq-mathcomp-word
Yet Another Coq Library on Machine Words
coq-coqeal
CoqEAL - The Coq Effective Algebra Library
coq-mathcomp-multinomials
Compatibility package for rocq-mathcomp-multinomials
rocq-mathcomp-multinomials
A Multivariate polynomial Library for the Mathematical Components Library
community
Start Contributing
Learn how to publish your first Rocq opam package today and make it available to the rest of the community.
