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 Makefile Scheme Other
Pull request Compare This branch is 24 commits ahead, 1139 commits behind coq:trunk.
Latest commit e446ce8 Jun 20, 2016 @mattam82 Rebase on trunk, new syntax for Hint Cut.
Also try to improve the subrelation_tac tactic
to start with the resolution of the most constrained
goals first, w/o affecting completeness thanks to goal
cycling.
Permalink
Failed to load latest commit information.
checker Fixing the checker. Jun 18, 2016
config Merge branch 'v8.5' Jan 21, 2016
dev Merge branch 'v8.5' Jun 9, 2016
doc par: like all: but in parallel Jun 17, 2016
engine Document new Hint Mode option. Jun 16, 2016
grammar remove grammar/grammar.mllib Jun 8, 2016
ide ideslave: do not bail out in case of XML error Jun 16, 2016
interp Exporting a generic argument induction_arg. As a consequence, Jun 18, 2016
intf Exporting a generic argument induction_arg. As a consequence, Jun 18, 2016
kernel Reuse the typing_flags datatype for inductives. Jun 18, 2016
lib remote counter: avoid thread race on sockets (fix #4823) Jun 17, 2016
library Reuse the typing_flags datatype for inductives. Jun 18, 2016
ltac Fix rewriting under binders Jun 18, 2016
man Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti … Jan 15, 2016
parsing Exporting a generic argument induction_arg. As a consequence, Jun 18, 2016
plugins Genrew: Add heterogeneous relations. Jun 18, 2016
pretyping Indentation Jun 18, 2016
printing Moving the typing_flags to the environment. Jun 18, 2016
proofs Add documentation for goal selectors. Jun 14, 2016
stm Moving the typing_flags to the environment. Jun 18, 2016
tactics Adding an "as" clause to specialize. Jun 18, 2016
test-suite Fix rewriting under binders Jun 18, 2016
theories Rebase on trunk, new syntax for Hint Cut. Jun 19, 2016
tools ocamllibdep + coqdep : simpler deps concerning .mllib and .mlpack Jun 15, 2016
toplevel Reuse the typing_flags datatype for inductives. Jun 18, 2016
.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 Ignore generated .ml file for ssrmatching Jun 16, 2016
.mailmap Update the .mailmap file. Oct 5, 2015
.merlin Add stm dir to .merlin Jun 18, 2016
CHANGES Giving a more natural semantics to injection by default. Jun 18, 2016
COMPATIBILITY Merge branch 'v8.5' May 20, 2016
COPYRIGHT ssrmatching: giving proper credits to the original author(s) Jun 15, 2016
CREDITS ssrmatching: giving proper credits to the original author(s) Jun 15, 2016
INSTALL Updating OCaml version number needed for 8.6. Apr 17, 2016
INSTALL.doc More on how to compile doc. Nov 6, 2015
INSTALL.ide Update required OCaml version in configure. May 26, 2016
LICENSE fix pour install windows Nov 9, 2005
Makefile Compilation via pack for plugins of the stdlib Jun 8, 2016
Makefile.build Makefile.build: ensure a build failure in case of a missing rule Jun 15, 2016
Makefile.checker Makefile.build split in many smaller files : Makefile.{ide,checker,de… Jun 8, 2016
Makefile.common Fix Makefile after ssrmatching merge Jun 16, 2016
Makefile.dev Makefile.build split in many smaller files : Makefile.{ide,checker,de… Jun 8, 2016
Makefile.doc Makefile.build split in many smaller files : Makefile.{ide,checker,de… Jun 8, 2016
Makefile.ide Makefile.build: ensure a build failure in case of a missing rule Jun 15, 2016
Makefile.install Makefile.build split in many smaller files : Makefile.{ide,checker,de… Jun 8, 2016
README.doc Remove some outdated files and fix permissions. Jul 31, 2015
README.md Description added Aug 5, 2015
README.win Win: update README Feb 14, 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 configure: use ln on linux and cp on windows Jun 14, 2016
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.