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:
-
530
Packages
-
10
New packages this month
-
40
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-robot-rocq
Formal Foundations for Modeling Robot Manipulators
coq-mathcomp-boot
Compatibility package for rocq-mathcomp-boot
coq-mathcomp-order
Compatibility package for rocq-mathcomp-order
rocq-mathcomp-boot
Small Scale Reflection
rocq-mathcomp-order
Mathematical Components Library on order theory
Recently Updated
coq-vcfloat
VCFloat: Floating Point Round-off Error Analysis
coq-vst
Verified Software Toolchain
rocq-robot-rocq
Formal Foundations for Modeling Robot Manipulators
coq-fourcolor-reals
Interface for real numbers used in the Four Color Theorem
coq-fourcolor
Mechanization of the Four Color Theorem in Coq
community
Start Contributing
Learn how to publish your first Rocq opam package today and make it available to the rest of the community.