Rocq Packages

Explore hundreds of Rocq packages with their documentation

Standard Library

Install Rocq Packages
Learn how to install and search for Rocq packages using opam, including extensions, libraries, and tools

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

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:

  • 577

    Packages

  • 2

    New packages this month

  • 9

    Updates this week

packages

coq-mathcomp-ssreflect

Compatibility package for rocq-mathcomp-ssreflect

Used by 44 other packages

coq-mathcomp-algebra

Compatibility package for rocq-mathcomp-algebra

Used by 31 other packages

coq-flocq

A formalization of floating-point arithmetic for the Coq system

Used by 19 other packages

coq-ext-lib

A library of Coq definitions, theorems, and tactics

Used by 16 other packages

coq-hierarchy-builder

Compatibility package for rocq-hierarchy-builder

Used by 16 other packages

rocq-induction

A better induction tactic for Rocq

28 hours ago

rocq-sail-stdpp

Support library for Sail, a language for describing the instruction semantics of processors, using stdpp bitvectors

2 weeks ago

rocq-induction

A better induction tactic for Rocq

Version 0.1.0+9.2

rocq-vellvm

Rocq library implementing (executable) semantics for LLVM IR

Version v3.0.20260707

coq-hammer-tactics

Reconstruction tactics for the hammer for Coq

Version 1.3.3+9.2

coq-hammer

General-purpose automated reasoning hammer tool for Coq

Version 1.3.3+9.2

coq-hott

The Homotopy Type Theory library

Version 9.1

community

Start Contributing

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

Publish a Rocq Package