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:
-
522
Packages
-
5
New packages this month
-
10
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-equations
Compatibility package, see rocq-equations
New Packages
rocq-aac-tactics
Rocq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators
rocq-hollight-logic
HOL-Light library necessary for translating unify
rocq-rouche-capelli
A proof for the Rouché–Capelli theorem by rocq-math-comp
rocq-libhyps
Hypotheses manipulation library
rocq-mathcomp-hollight-real-with-N
HOL-Light definition of real numbers in Rocq using N and MathComp
Recently Updated
coq-formalv-check_range
Tactics to automatically prove Boolean goals involving Uint63/Sint63 variables
coq-formalv-prim63_mathcomp
Refinements from MathComp nat and int to Coq primitive integers Uint63/Sint63
coq-formalv-time
A Coq library for time and date arithmetic according to the UTC standard with leap seconds
coq-bedrock2-compiler
A work-in-progress language and compiler for verified low-level programming (compiler part)
rocq-aac-tactics
Rocq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators
community
Start Contributing
Learn how to publish your first Rocq opam package today and make it available to the rest of the community.
