Coq 8.4 is available in beta testing. It 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, 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. Please report manifest regressions not mentioned in the CHANGES file.

The Reference Manual for Coq 8.4 is browsable online but is not yet fully up-to-date. The standard library is here.

Sources
	coq-8.4beta2.tar.gz	4 MB
Binaries
Windows	coq-installer-8.4beta2-0.exe (bundled with CoqIDE)	54 MB
MacOS	coq-8.4beta2.dmg	81 MB
	coqide-8.4beta2.dmg (Coq bundled with CoqIDE interface)	92 MB
	The packages require MacOS ≥ 10.5

On Linux, BSD or MacOS package-based distributions, Coq is released by the corresponding maintainers. For reports on the Windows package and the MacOS dmg packages, use the Coq bug tracker.