Core components of the coq 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.

This package includes the Coq core binaries, plugins, and tools, but not

the vernacular standard library.

Version: 8.16.1

## 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 programs |

coqdoc | A documentation tool for the Coq proof assistant |

coqnative | The Coq native compiler |

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 |