The current version: Coq 8.4pl4

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)

coq-8.4pl4.tar.gz 4 MB
coq-installer-8.4pl4.exe (bundled with CoqIDE) (sha1, sig) 54 MB
coqide-8.4pl4.dmg (bundled with CoqIDE interface) 94 MB
The above packages are for MacOS ≥ 10.5 (bundled with CoqIDE interface) 84 MB
coqide-8.4pl4-ssreflect-1.5.dmg (bundled with CoqIDE interface and ssreflect plugin) 93 MB
The above packages are experimental packages for MacOS ≥ 10.7; Coq 8.4pl4 is otherwise available through MacPorts and Homebrew
0.2 MB
Reference-Manual.pdf 1.5 MB
Previous and Development versions of Coq

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:// 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.

Extensions of Coq

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:

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).