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
-
4
New packages this month
-
14
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
rocq-categories
A library for category theory
rocq-partial-orders
A library for setoids, partial orders, complete lattices and related structures
Recently Updated
rocq-metarocq-common
The common library of Template Rocq and PCUIC
rocq-metarocq-erasure-plugin
Implementation and verification of an erasure procedure for Rocq
rocq-metarocq-erasure
Implementation and verification of an erasure procedure for Rocq
rocq-metarocq-pcuic
A type system equivalent to Rocq's and its metatheory
rocq-metarocq-quotation
Gallina quotation functions for Template Rocq
community
Start Contributing
Learn how to publish your first Rocq opam package today and make it available to the rest of the community.
