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 C Shell C++ Emacs Lisp
Pull request Compare This branch is 877 commits behind HoTT:trunk.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
checker still some more dead code removal Oct 6, 2012
config Repair the configure after Hugo's last "repair" ;-) Oct 5, 2012
dev Turn mltop.ml4 into a regular ocaml file Oct 6, 2012
doc Move reflexivity, symmetry, and transitivity, next to f_equal, in the… Sep 16, 2012
grammar remove useless hidden_flag in TacMutual(Co)Fix Oct 6, 2012
ide MacOS integration uses lablgtkosx >= 1.1 Sep 17, 2012
interp Remove some more "open" and dead code thanks to OCaml4 warnings Oct 2, 2012
intf remove useless hidden_flag in TacMutual(Co)Fix Oct 6, 2012
kernel Merge with trunk, again Oct 12, 2012
lib avoid using rectypes in dnet.ml Oct 6, 2012
library Merge with trunk, again Oct 12, 2012
man Coqtop and coqc: cleaning description of options in RefMan and manpages. Jan 21, 2012
parsing restore compatibility with camlp5 < 6.00 Oct 6, 2012
plugins still some more dead code removal Oct 6, 2012
pretyping Merge with trunk, again Oct 12, 2012
printing still some more dead code removal Oct 6, 2012
proofs still some more dead code removal Oct 6, 2012
scripts Merge with trunk, again Oct 12, 2012
tactics still some more dead code removal Oct 6, 2012
test-suite test-suite: fix grep rule for output tests Sep 4, 2012
theories Revert "En cours pour 'generalize in clause' et 'induction in clause'" Oct 4, 2012
tools fix r15860 : no slash after $(COQLIB) Oct 8, 2012
toplevel Merge with trunk, again Oct 12, 2012
.dir-locals.el Added .dir-locals file to take advantage of emacs 23's new Directory-… Aug 1, 2011
.gitignore Turn mltop.ml4 into a regular ocaml file Oct 6, 2012
.typerex Tentative and very experminental support for typerex. Enabled with May 11, 2012
CHANGES CHANGES: document the end of states/initial.coq and coqtop.opt Aug 23, 2012
COMPATIBILITY Some extra INCOMPATIBILITIES since 8.4. Aug 11, 2012
COPYRIGHT Fixed #2789. May 25, 2012
CREDITS Vernacexpr is now a mli-only file, locality stuff now in locality.ml May 29, 2012
INSTALL No more states/initial.coq, instead coqtop now requires Prelude.vo Aug 23, 2012
INSTALL.doc Amélioration du README.doc et de l'installation de la doc Nov 14, 2008
INSTALL.ide Bug 2823: update INSTALL.ide in order to ask for lablgtksourceview Jun 20, 2012
INSTALL.macosx MAJ ppc/i386 Apr 24, 2007
LICENSE fix pour install windows Nov 9, 2005
Makefile Remove broken makefile option NO_RECOMPILE_LIB Sep 20, 2012
Makefile.build Turn mltop.ml4 into a regular ocaml file Oct 6, 2012
Makefile.common Moved Compat to parsing. This permits to break the dependency of the Oct 4, 2012
Makefile.doc configure: get rid of the -src option and of ${COQSRC} Aug 23, 2012
README - changing minimal version for OCaml: Coq uses Filename.dirsep that i… Feb 20, 2012
README.doc Mise à jour des fichiers README et INSTALL de la doc (bug #1921) + su… Aug 6, 2008
README.win Win32: remove the need for Coq.bat and Coqide.bat Apr 21, 2011
TODO git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9415 85f007b7… Dec 8, 2006
_tags Turn mltop.ml4 into a regular ocaml file Oct 6, 2012
build Minor fix in the ./build wrapper for ocamlbuild Oct 6, 2012
configure Turn mltop.ml4 into a regular ocaml file Oct 6, 2012
coq-win32.itarget Win32 cross-compilation from debian: build of coqide.exe and other bi… Feb 24, 2010
coq.itarget Ocamlbuild: try to speed-up error detection in *.ml*, by byte-compili… Jun 3, 2010
install.sh Remove bashisms Jan 28, 2010
myocamlbuild.ml Turn mltop.ml4 into a regular ocaml file Oct 6, 2012

README

               	         THE COQ V8 SYSTEM
            	         =================

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 http://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 at http://coq.inria.fr, or, for older versions at
   ftp://ftp.inria.fr/INRIA/LogiCal/coq.


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 submission
   address is:

	coq-club@inria.fr

   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.

   To be added to, or removed from, the mailing list, please write to:

	coq-club-request@inria.fr

   Please use also this address for any questions/suggestions about the
   Coq Club. It might sometimes take a few days before your messages get
   forwarded.


BUGS REPORT.
============

   Send your bug reports by filling a form at

        http://coq.inria.fr/bugs

   To be effective, bug reports should mention the Caml 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.