Proof management system

Coq is a formal proof management system. 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.

Version: 8.13.2

See also: coq-coqide.

## General Commands | |

coq-tex | Process Coq phrases embedded in LaTeX files |

coq_makefile | The Coq Proof Assistant makefile generator |

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 |

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 |