package rocq-primitive

  1. Overview
  2. Doc
Rocq primitive object OCaml library

Install

Dune Dependency

Authors

Maintainers

Sources

rocq-primitive-9.0.0.tar.gz
sha512=308c1917bd8b011b4deed84c0fe5912831e4ce72a3ef9c72d89a9d09b68d65eefdd4ca4ded00ffa4db6620e8ba0fb037214ba41e03d9ab129348241e015fbbfb

Description

This library provides OCaml modules for primitive objects in the Rocq Prover. These modules can be used in Rocq-based projects that rely on extraction to OCaml.

Published: 26 Jan 2026

Dependencies (3)

  1. ocamlfind >= "1.8.1"
  2. ocaml >= "4.09.0"
  3. dune >= "2.9"

Dev Dependencies (1)

  1. odoc with-doc

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover