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 C Shell Makefile Other
Pull request Compare This branch is 2381 commits behind coq:master.
Latest commit 078598d Feb 3, 2017 @maximedenes maximedenes Merge PR#418: Travis CI configuration
Commits were squashed.
Permalink
Failed to load latest commit information.
checker Moving unused code out of the kernel into Termops. Oct 31, 2016
config Fix some documentation typos. Nov 24, 2016
dev Adding a printer for Proof.proof reflecting the focusing layout. Jan 26, 2017
doc Merge branch 'v8.6' Jan 19, 2017
engine Merge branch 'v8.6' Feb 1, 2017
grammar Merge branch 'v8.6' into trunk Nov 3, 2016
ide Merge branch 'v8.6' Feb 1, 2017
interp Merge branch 'v8.6' Feb 1, 2017
intf Adding a new evar source to remember the name of evars which were Jan 22, 2017
kernel Merge branch 'v8.6' Feb 1, 2017
lib Merge branch 'v8.6' Feb 1, 2017
library Use Pp.quote in string options. Dec 19, 2016
ltac Merge branch 'v8.6' Feb 1, 2017
man Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti … Jan 15, 2016
parsing Merge branch 'v8.6' Dec 7, 2016
plugins Merge branch 'v8.6' Jan 19, 2017
pretyping Merge branch 'v8.6' Feb 1, 2017
printing Merge branch 'v8.6' Feb 1, 2017
proofs Adding a printer for Proof.proof reflecting the focusing layout. Jan 26, 2017
stm Merge branch 'v8.6' Feb 1, 2017
tactics Fixing injection in the presence of let-in in constructors. Dec 22, 2016
test-suite Merge branch 'v8.6' Feb 1, 2017
theories Fix a typo in Hurkens.v comment Dec 19, 2016
tools Merge branch 'v8.6' Jan 19, 2017
toplevel Merge branch 'v8.6' Feb 1, 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 Merge branch 'v8.6' Oct 24, 2016
.mailmap Deduplicate some names in .mailmap Jul 6, 2016
.merlin Merge branch 'v8.6' Dec 7, 2016
.travis.yml Travis CI configuration. Runs validate & test-suite. Feb 3, 2017
CHANGES Merge branch 'v8.6' Jan 19, 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 [build] META file to enable plugin linking with ocamlfind. Oct 28, 2016
Makefile Merge branch 'v8.6' Dec 7, 2016
Makefile.build Converting certain "order-only" (Makefile) dependencies to regular de… Oct 19, 2016
Makefile.checker Revert "Merge remote-tracking branch 'github/pr/229' into trunk" Jul 5, 2016
Makefile.common Revert "Merge remote-tracking branch 'github/pr/229' into trunk" Jul 5, 2016
Makefile.dev Merge branch 'v8.6' Sep 1, 2016
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 [build] Add a target to install the META file. Oct 28, 2016
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.ml: our configure script is now written in ML :-) Dec 20, 2013
configure.ml Merge branch 'v8.6' Jan 19, 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.