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
-
5
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-interval
A Coq tactic for proving bounds on real-valued expressions automatically
coq-coqprime
Compatibility metapackage for CoqPrime library after the Rocq renaming
rocq-coqprime
Certifying prime numbers in Rocq
rocq-navi
Extension of coq2html Document Generator
coq-rewriter
Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography
community
Start Contributing
Learn how to publish your first Rocq opam package today and make it available to the rest of the community.
