Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
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 Other

This branch is 493 commits ahead, 3796 commits behind coq:trunk

- Relax identification of metas in Ltac to not compare universes synt…

…actically.

- add constr_eq_nounivs tactic to compare constrs without comparing universes.
latest commit e88e47ca76
@mattam82 mattam82 authored
Failed to load latest commit information.
checker This commit adds full universe polymorphism to Coq.
config New -no-native-compiler flag for configure, globally disabling the na…
dev This commit adds full universe polymorphism to Coq.
doc Small doc fix : module subtyping cannot force access of opaques
grammar This commit adds full universe polymorphism to Coq.
ide Better encapsulation of MessageView
interp Merge with recent trunk and new version of universe polymorphism.
intf after conflict resolution
kernel Enforce Prop < Set directly in the universe graph (fixes #50).
lib This commit adds full universe polymorphism to Coq.
library Enforce Prop < Set directly in the universe graph (fixes #50).
man Coqtop and coqc: cleaning description of options in RefMan and manpages.
parsing Fix [change] forgeting about universes in the right-hand-side (#36) a…
plugins - Use oracle transparent state everywhere during unification, properly
pretyping - Relax identification of metas in Ltac to not compare universes synt…
printing Print universe polymorphism information for parameters as well.
proofs - Use oracle transparent state everywhere during unification, properly
scripts This commit adds full universe polymorphism to Coq.
tactics - Relax identification of metas in Ltac to not compare universes synt…
test-suite This commit adds full universe polymorphism to Coq.
theories - Use oracle transparent state everywhere during unification, properly
tools Restrict (try...with...) to avoid catching critical exn (part 15)
toplevel Merge ../../coq/git into trunk
.dir-locals.el Fixing emacs diff bug with .dir-locals.el.
.gitignore This commit adds full universe polymorphism to Coq.
.typerex Tentative and very experminental support for typerex. Enabled with
CHANGES Using hnf instead of "intro H" for forcing reduction to a product.
COMPATIBILITY Some extra INCOMPATIBILITIES since 8.4.
COPYRIGHT Fixed #2789.
CREDITS Vernacexpr is now a mli-only file, locality stuff now in locality.ml
INSTALL No more states/initial.coq, instead coqtop now requires Prelude.vo
INSTALL.doc Amélioration du README.doc et de l'installation de la doc
INSTALL.ide Bug 2823: update INSTALL.ide in order to ask for lablgtksourceview
INSTALL.macosx MAJ ppc/i386
LICENSE fix pour install windows
Makefile This commit adds full universe polymorphism to Coq.
Makefile.build Checker: re-sync vo structures after Maxime's commit 16136
Makefile.common New implementation of the conversion test, using normalization by eva…
Makefile.doc configure: get rid of the -src option and of ${COQSRC}
README - changing minimal version for OCaml: Coq uses Filename.dirsep that i…
README.doc Mise à jour des fichiers README et INSTALL de la doc (bug #1921) + su…
README.win Win32: remove the need for Coq.bat and Coqide.bat
TODO git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9415 85f007b7…
_tags Revert "remove -rectypes except for term.ml"
build Minor fix in the ./build wrapper for ocamlbuild
configure New -no-native-compiler flag for configure, globally disabling the na…
coq-win32.itarget Win32 cross-compilation from debian: build of coqide.exe and other bi…
coq.itarget Ocamlbuild: try to speed-up error detection in *.ml*, by byte-compili…
install.sh Remove bashisms
myocamlbuild.ml Revert "remove -rectypes except for term.ml"

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.
Something went wrong with that request. Please try again.