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.
OCaml Coq TeX Shell C Makefile Other
Permalink
Failed to load latest commit information.
checker [pp] Remove uses of expensive string_of_ppcmds. Mar 21, 2017
config Fix some documentation typos. Nov 24, 2016
dev [travis] Add VST Mar 24, 2017
doc Merge PR#433: doc: fix a French-ism Mar 23, 2017
engine [pp] Remove uses of expensive string_of_ppcmds. Mar 21, 2017
grammar Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5. Mar 22, 2017
ide make check not CoqIDE-specific Mar 22, 2017
interp [safe_string] interp/dumpglob Mar 14, 2017
intf Attempt to improve error message when "apply in" fail. Mar 15, 2017
kernel Merge branch 'v8.6' into trunk Mar 24, 2017
lib Merge branch 'v8.6' into trunk Mar 24, 2017
library Merge PR#390: Updates to the Pretty Printing Infrastructure Mar 22, 2017
man Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti … Jan 15, 2016
parsing Merge branch 'v8.6' Mar 22, 2017
plugins Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#… Mar 23, 2017
pretyping Merge branch 'v8.6' into trunk Mar 23, 2017
printing [pp] Move terminal-specific tagging to the toplevel. Mar 21, 2017
proofs [pp] [ide] Minor cleanups in pp code. Mar 21, 2017
stm [xml] Restore protocol compatibility with 8.6. Mar 21, 2017
tactics Merge branch 'v8.6' into trunk Mar 23, 2017
test-suite Merge branch 'v8.6' into trunk Mar 23, 2017
theories Merge PR#392: strengthened the statement of JMeq_eq_dep Mar 24, 2017
tools Merge branch 'v8.6' Mar 22, 2017
toplevel Merge PR#390: Updates to the Pretty Printing Infrastructure Mar 22, 2017
vernac Merge branch 'v8.6' Mar 22, 2017
.dir-locals.el Don't set global variables from a hidden file. (!) Jul 14, 2014
.gitattributes gitattributes: add `.mailmap` file to the list of files excluded from… Mar 16, 2015
.gitignore Improve build of travis target on local machine. Mar 10, 2017
.mailmap Deduplicate some names in .mailmap Jul 6, 2016
.merlin [safe-string] Enable -safe-string ! Mar 14, 2017
.travis.yml [travis] Add VST Mar 24, 2017
CHANGES Document the changes to IZR. Mar 22, 2017
COMPATIBILITY Being more informative about the change of behavior of "subst". Sep 29, 2016
COPYRIGHT Merge branch 'v8.5' into v8.6 Jul 13, 2016
CREDITS ssrmatching: giving proper credits to the original author(s) Jun 15, 2016
INSTALL Relax required OCaml to 4.02.1. Jan 9, 2017
INSTALL.doc More on how to compile doc. Nov 6, 2015
INSTALL.ide Relax required OCaml to 4.02.1. Jan 9, 2017
LICENSE fix pour install windows Nov 9, 2005
META.coq [META] add support for ide libraries Mar 22, 2017
Makefile [travis] [External CI] Script renaming. Feb 7, 2017
Makefile.build [xml] Restore protocol compatibility with 8.6. Mar 21, 2017
Makefile.checker Revert "Merge remote-tracking branch 'github/pr/229' into trunk" Jul 5, 2016
Makefile.ci [travis] Add VST Mar 24, 2017
Makefile.common Fixing dependency order of plugins. Mar 9, 2017
Makefile.dev Ltac as a plugin. Feb 17, 2017
Makefile.doc Avoid concurrent runs when producing html documentation (bug #5269). Dec 19, 2016
Makefile.ide Revert "Merge remote-tracking branch 'github/pr/229' into trunk" Jul 5, 2016
Makefile.install [META] [build] Install dlls to kernel/byterun Mar 10, 2017
README.ci [travis] Move ci files from `tools` to `dev`. Feb 7, 2017
README.doc Remove some outdated files and fix permissions. Jul 31, 2015
README.md Description added Aug 5, 2015
TODO Switch the few remaining iso-latin-1 files to utf8 Dec 9, 2014
configure configure: avoid deprecated warnings Feb 7, 2017
configure.ml [safe-string] Enable -safe-string ! Mar 14, 2017
install.sh Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins … Dec 17, 2014

README.md

Coq

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.

Installation

See the file INSTALL for installation procedure.

Documentation

The documentation is part of the archive in directory doc. The documentation of the last released version is available on the Coq web site at coq.inria.fr/doc.

Changes

There is a file named CHANGES that explains the differences and the incompatibilities since last versions. If you upgrade Coq, please read it carefully.

Availability

Coq is available from coq.inria.fr.

The Coq Club

The Coq Club moderated mailing list is meant to be a standard way to discuss questions about the Coq system and related topics. The subscription link can be found at coq.inria.fr/community.

The topics to be discussed in the club should include:

  • technical problems;
  • questions about proof developments;
  • suggestions and questions about the implementation;
  • announcements of proofs;
  • theoretical questions about typed lambda-calculi which are closely related to Coq.

For any questions/suggestions about the Coq Club, please write to coq-club-request@inria.fr.

Bugs report

Send your bug reports by filling a form at coq.inria.fr/bugs.

To be effective, bug reports should mention the OCaml version used to compile and run Coq, the Coq version (coqtop -v), the configuration used, and include a complete source example leading to the bug.