Package coq-core-compat
Compatibility binaries for Coq after the Rocq renaming
Rocq 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 compatibility binaries to call Rocq
through previous Coq commands like coqc coqtop,...
Version: 9.1.1
General Commands | |
| coq-tex | process Coq phrases embedded in LaTeX files |
| coq_makefile | generate makefiles for Coq proof development |
| coqc | Coq compiler |
| coqchk | verify compiled Coq libraries |
| coqdep | compute inter-module dependencies for Coq programs |
| coqdoc | documentation tool for the Coq proof assistant |
| coqnative | native Coq compiler |
| coqtop | toplevel Coq system |
| coqtop.byte | bytecode toplevel Coq system |
| coqwc | print the number of specification, proof and comment lines in Coq files |