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,

Coqide.

Command | Description |
---|---|

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 |

gallina | extracts specification from Coq vernacular files |