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:
-
590
Packages
-
6
New packages this month
-
18
Updates this week
packages
Most Used
rocq-stdlib
The Rocq Proof Assistant -- Standard Library
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
New Packages
rocq-coqprime
Certifying prime numbers in Rocq
rocq-hollight
HOL-Light library in Rocq
rocq-mathcomp-zify
Micromega tactics for Mathematical Components
rocq-robust-geometric-predicates
Machine-checked robust binary64 geometric predicates, sound vs. exact arithmetic
rocq-spatial-algebra
DE-9IM intersection-matrix algebra and integer orientation-determinant bounds (axiom-free)
Recently Updated
coq-coqprime
Compatibility metapackage for CoqPrime library after the Rocq renaming
rocq-coqprime
Certifying prime numbers in Rocq
rocq-hollight
HOL-Light library in Rocq
rocq-navi
Extension of coq2html Document Generator
rocq-robot-rocq
Formal Foundations for Modeling Robot Manipulators
community
Start Contributing
Learn how to publish your first Rocq opam package today and make it available to the rest of the community.
