Download
This version features:
- a new modular and uniform extension of the arithmetical libraries by P. Letouzey which systematically provides power, gcd/lcm, square root, base 2 logarithm, division, modulo, bitwise operators, logical shift, comparisons, iterators for all of nat, N, Z, BigN and BigZ on top of a uniform naming layer (e.g. plus and mult are now consistently named add and mul while still remaining mostly compatible with 8.3) (example 1, example 2, example 3);
- a new proof engine by A. Spiwack whose most salient feature is the introduction of bullets (+, -, *) and structured scripts ({ ... }) (example).
The main other changes are:
- addition of eta-conversion to the logic;
- a slightly more flexible guard condition for fixpoints;
- a more systematic support for pattern-matching on dependent types;
- more robust CoqIDE (including a new communication protocol by V. Gross);
- a new library of vectors (lists of a given length);
- support for referring to expressions of the goal using pattern in tactics;
- automatic computation of occurrences to abstract over in destruct/induction (example);
- various improvements to Ltac (timeout, appcontext, constr_eq, is_evar, has_evar, generic match _ with _ => _ end pattern, fine-tuning of simpl);
- implicit arguments in anonymous functions;
- notations with binders (e.g. exists x y z : A, P x y z) (example);
- many bug fixes and improvements of existing features (type classes, setoid rewriting, ring, nsatz, micromega, extraction, Function, module system, coq_makefile, ...);
For a full log of changes, see the file CHANGES.
Coq 8.4 is not entirely upward compatible with 8.3 (see main incompatibilities)
| Sources | ||
| coq-8.4pl6.tar.gz | 4 MB | |
| Binaries | ||
 Windows |
coq-installer-8.4pl6.exe (bundled with CoqIDE) (sha1, sig) | 54 MB |
 MacOS |
coqide-8.4pl5.dmg (bundled with CoqIDE interface) | 98 MB |
| The above packages are packages for MacOS 10.9; versions of Coq are otherwise available through MacPorts, Homebrew, Fink, ... | ||
| Documentation | ||
| Tutorial.pdf | 0.2 MB | |
| Reference-Manual.pdf | 1.5 MB | |
The previous stable releases of the Coq system are the version 8.3 and version 8.2.
The development version of Coq is browsable and downloadable from our Git repository using command: git clone git://scm.gforge.inria.fr/coq/coq.git. The daily level of stability of this version (and of the bug-fix branches) can be observed at the coq-bench site or by subscribing to the coq-bench mailing list.
Most of the previous version of Coq are available here.
When compiled with Objective Caml 3.11 (which is the case of the Windows and MacOS packages we release), Coq supports dynamic loading of extensions. The following extensions are known to work as plugins:
- The small scale reflection package (ssreflect) contains the robust and compact tactic language and libraries that were started for supporting the full formalization of the 4 color theorem and that now serves, among other applications, as support for the ongoing formalization of the odd order theorem in group theory. (*)
- The rewriting modulo associativity and commutativity plugin (AAC_tactics). (*)
- The classical extraction module provides extraction of programs from classical proofs in Prop.
- The rippling plugin for automation of inductive arguments.
- The descente infinie plugin for delayed inference of the induction hypothesis needed in well-founded induction. (*)
Note: Objective Caml ≥ 3.11.1 is required for building plugins on MacOS 10.5. (*) above means that the plugin is submitted to the user contributions and planned to be kept compatible with the new releases of Coq to come.
Consider also the experimental Coq Modulo Theories (CoqMT) which modifies Coq with primitive support for user-defined first-order equational theories (starting with linear arithmetic).