The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Dear Coq-Club members,

We are pleased to announce that the final release of Coq 8.4 is now
available at http://coq.inria.fr/. We remind its main features:

- a 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, 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);
- a new proof engine by A. Spiwack whose most salient feature is the
  introduction of bullets (+, -, *) and structured scripts ({ ... }).

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);
- a new library of finite sets based on red-black trees (A. Appel);
- support for referring to expressions of the goal using pattern in tactics;
- automatic computation of occurrences to abstract over in destruct/induction;
- various improvements to Ltac (timeout, eq_constr, is_evar, has_evar, 
  generic "match _ with _ => _ end" pattern, fine-tuning of simpl);
- implicit arguments in anonymous functions;
- notations with iterated binders (e.g. "exists x y z : A, P x y z");
- many improvements of existing features (type classes, setoid rewriting,
  ring, nsatz, micromega, extraction, Function, module system,
  coq_makefile, coqide, coqdoc, backtracking, ...);
- many bug fixes and refinements, especially w.r.t. 8.4 beta
  (proof engine and existential variables, "Show Script", alternative
  info tactical, ...).

See http://coq.inria.fr/ for more details.

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.

New extension packages we are aware about include the following (but
probably there are more):

Equations (M. Sozeau):
  Dependent pattern-matching compiler and specification generator 
Ergo (S. Lescuyer):
  Reflexive tactic for SMT solving 
Nfix (S. Lescuyer):
  Extension for fixpoints on nested inductives
Counting (S. Lescuyer):
  Collecting statistics on size of definitions/proofs
RelationExtraction (C. Dubois, D. Delahaye, P.-N. Tollitte):
  Function extraction from inductive relations
Paco (C.-K. Hur, G. Neis, D. Dreyer, V. Vafeiadis):
  Parameterized coinduction

Note also the following (non-plugin) user contributions submitted
since 8.3 was released:

RegExp (T. Miyamoto):
  Library for regular expression based on Brzozowski's algorithm
MathClasses (B. Spitters, E. van der Weegen, R. Krebbers):
  Typeclass-based foundational interfaces for formalized constructive
  mathematics
Containers (S. Lescuyer):
  A typeclass-based library of finite sets/maps
ZornsLemma (D. Schepler):
  Basic set theory
Topology (D. Schepler):
  Basic concepts and results of general topology
FreeGroups (D. Schepler):
  Van der Waerden's proof about free group on set of generators
EuclidianGeometry (J. Duprat):
  Basis of the Euclid's plane geometry
PTSATR (V. Siles):
  Equivalence of PTS with or without judgemental equality
GenericEnvironments (E. Polonovski):
  A library providing an abstract data type of environments

The Coq Development Team