Rocq Packages
Explore hundreds of open-source Rocq packages with their documentation
Publish a Package
opam
The OCaml and Rocq Package Manager
Opam is a source-based package manager for OCaml and Rocq. It supports multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow
-
467
Packages
-
1
New packages this month
-
6
Updates this week
packages
Most Used
coq-mathcomp-ssreflect
Small Scale Reflection
coq-mathcomp-algebra
Mathematical Components Library on Algebra
coq-flocq
A formalization of floating-point arithmetic for the Coq system
coq-hierarchy-builder
High level commands to declare and evolve a hierarchy based on packed classes
coq-ext-lib
A library of Coq definitions, theorems, and tactics
New Packages
coq-hol-light-real-with-N
Definition of HOL-Light real numbers in Coq using N
Recently Updated
coq-vcfloat
VCFloat: Floating Point Round-off Error Analysis
coq-vst-lib
VSTlib: VST-verified C library for VST-verified clients
coq-libvalidsdp
LibValidSDP
coq-validsdp
ValidSDP
coq-library-fol
A Coq Library for First-Order Logic
community
Start Contributing
Learn how to publish your first Opam package today and make it available to the rest of the community.
