The Coq mailing list

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

Dear Coq-Club members,

We are pleased to announce that a beta-release of Coq 8.4 is available
at http://coq.inria.fr/. 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, 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);
- 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 bug fixes and improvements of existing features (type classes,
  setoid rewriting, nsatz, micromega, extraction, Function, module
  system, coq_makefile, ...).

See http://coq.inria.fr/coq-84 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 Bruno Barras, Frédéric
Besson, Pierre Corbineau, Pierre Courtieu, Julien Forest, Benjamin
Grégoire, 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, Cédric Auger,
David Baelde, Dan Grayson, Paolo Herms, Robbert Krebbers, Marc Lasson,
Hendriks Tews and Eelis van der Weegen.