libcoq-stdlib
proof assistant for higher-order logic (theories)
Coq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal
specification. It is developed using Objective Caml and Camlp5.
coq-dpdgraph-tools
Coq plugin to extract dependencies between Coq objects (tools)
This package provides a plugin for Coq to extract dependencies
between Coq objects and produce files with dependency information.
libcoq-equations
Coq library to work with functions defined by equations
This library provides a notation to write programs using dependent
pattern-matching and well-founded recursion in Coq.
libcoq-hott
Coq library for homotopy type theory
This library is a formalization of homotopy type
theory for Coq, where propositional equality is
interpreted as homotopy and type isomorphism as
homotopy equivalence.
libcoq-serapi-ocaml
interaction with Coq (runtime)
SerAPI provides a library for machine-to-machine
interaction with Coq with particular emphasis on
integrated development environments, code analysis tools
and machine learning.
libcoq-coquelicot
Coq library for real analysis
This package provides a formalization of real analysis compatible
with the Coq standard library.