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, 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.4 is the result of the work of many people. The main developers involved in 8.4 were Pierre Letouzey, Hugo Herbelin, Arnaud Spiwack, Matthieu Sozeau, Vincent Gross, Pierre Boutillier, Stéphane Glondu and Enrico Tassi with contributions also from Andrew Appel, Bruno Barras, Yves Bertot, Frédéric Besson, Pierre Corbineau, Pierre Courtieu, Julien Forest, Benjamin Grégoire, Robbert Krebbers, Assia Mahboubi (doc), Guillaume Melquiond, Jean-Marc Notin, Loïc Pottier, Pierre-Marie Pédrot, Matthias Puech, Yann Régis-Gianas, Vincent Siles and Élie Soubiran as well as patches from Tom Prince, Adam Chlipala, Cédric Auger, David Baelde, Dan Grayson, François Garillot, Nima Hoda, Paolo Herms, Robbert Krebbers, Marc Lasson, Adam Megacz, Benjamin Monate, Daniel de Rauglaudre, Hendriks Tews and Eelis van der Weegen.