package coq-core

  1. Overview
  2. No Docs
Compatibility binaries for Coq after the Rocq renaming

Install 

dune-project
 Dependency

rocq-prover.org Edit opam file Versions (14)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

Description

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching.

This package includes compatibility binaries to call Rocq through previous Coq commands like coqc coqtop,...

Added to opam-repository:

Dependencies (2)

  1. rocq-runtime = version
  2. dune >= "3.21"

Dev Dependencies (1)

  1. odoc with-doc

Used by (4)

  1. coq >= "9.3.0"
  2. coq-stdlib >= "9.0.0"
  3. prooftree
  4. why3-coq >= "1.8.2"

Conflicts

None