Rocq Packages

Explore hundreds of open-source Rocq packages with their documentation

Publish a Package

Learn how to publish your first opam package today and make it available to the rest of the community

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

470

Packages
3

New packages this month
2

Updates this week

packages

Most Used

coq-mathcomp-ssreflect

Small Scale Reflection

Used by 44 other packages

coq-mathcomp-algebra

Mathematical Components Library on Algebra

Used by 32 other packages

coq-flocq

A formalization of floating-point arithmetic for the Coq system

Used by 16 other packages

coq-hierarchy-builder

High level commands to declare and evolve a hierarchy based on packed classes

Used by 13 other packages

coq-ext-lib

A library of Coq definitions, theorems, and tactics

Used by 12 other packages

New Packages

coq-pil

Coq library for Propositional Intuitionistic Logic & Pitts Interpolation Library

2 weeks ago

coq-mk-choice-axiom-and-equivalent-propositions

Machine-Proof-of-the-Axiom-of-Choice-and-Its-Equivalent-Propositions

3 weeks ago

rocq-elpi

Elpi extension language for Coq