Package coq

Proof management system

Coq is a formal proof management system. It allows for the development
of theorems through first order logic that are mechanically checked by
the machine. Sets of definitions and theorems can be saved as compiled
modules and loaded into the system.

This package provides the main Coq binary without an optional IDE,

General Commands
Command Description
coqc The Coq Proof Assistant compiler
coqchk The Coq Proof Checker compiled libraries verifier
coqdep Compute inter-module dependencies for Coq and Caml programs
coqdoc A documentation tool for the Coq proof assistant
coqide The Coq Proof Assistant graphical interface
coq_makefile The Coq Proof Assistant makefile generator
coqmktop The Coq Proof Assistant user-tactics linker
coq-tex Process Coq phrases embedded in LaTeX files
coqtop The Coq Proof Assistant toplevel system
coqtop.byte The bytecode Coq toplevel
coqtop.opt The native-code Coq toplevel
coqwc print the number of specification, proof and comment lines in Coq files
gallina extracts specification from Coq vernacular files