The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Team,

many thanks for your efforts on further improving Coq!

You might want to mention in the change log the changes done with bug-fix 
3199 (cost for extern hints is actually taken into account). I have some 
files where this changed the eauto proof search time from a few seconds to 
infinite because some hint which can be repeated endlessly ended up having 
lower cost than a hint solving the goal. It is easy to fix the hint costs, 
but you have to know it.

Best regards,

Michael

-----Original Message-----
From: 
matthieu.sozeau AT gmail.com
 
[mailto:matthieu.sozeau AT gmail.com]
 On Behalf Of Matthieu Sozeau
Sent: Thursday, April 23, 2015 3:37 PM
To: 
coq-club AT inria.fr
Subject: [Coq-Club] Coq 8.5 beta 2

Dear Coq-Clubers,

  The Coq development team is pleased to announce the release of the second 
beta version of Coq 8.5 available at:

  http://coq.inria.fr/coq-85

  This new beta version includes many bug fixes with respect to the first 
beta version released in January, and a few incompatible changes, see the 
following file for more information:

  https://coq.inria.fr/distrib/V8.5beta2/CHANGES

Source, Windows and OS X packages are available.

We recall the new available features of version 8.5:

- asynchronous edition of documents under CoqIDE to keep working on a
  proof while Coq checks the other proofs in the background (by Enrico
  Tassi);
- universe polymorphism making it possible to reuse the same
  definitions at various universe levels (by Matthieu Sozeau);
- primitive projections improving space and time efficiency of
  records, and adding eta-conversion for records (by Matthieu Sozeau);
- extensions of the new proof engine featuring dependent subgoals
  management, fully backtracking tactics, as well as tactics which can
  consider multiple goals together (by Arnaud Spiwack);
- a new reduction procedure called native_compute to evaluate terms
  using the OCaml native compiler, for proofs with large computational
  steps (by Maxime Dénès).

The main other changes are:

- a new fast compilation chain that skips checking of proofs (producing
  .vio files);
- a new construct $(..)$ to call tactics from term definitions;
- a more restrictive guard condition to recover compatibility with axioms
  like propositional extensionality and (some consequences of) univalence;
- a new option -type-in-type to collapse the universe hierarchy (makes
  the logic inconsistent but useful for exploration);
- a better-behaved alternative to simpl, called cbn;
- various improvements to the tactic language, like a new introduction
  pattern [= x1 ... xn] which applies injection on the fly (inspired
  by SSReflect); new constructs uconstr:c and type_term c to build
  untyped terms in Ltac;
- significant improvements of general efficiency.

See http://coq.inria.fr/ for more details, and the CHANGES file in the 
distribution for a comprehensive list.

The Coq development team wishes to acknowledge the many people who made Coq 
8.5 possible: Pierre Boutillier, Pierre Courtieu, Maxime Dénès, Hugo 
Herbelin, Pierre Letouzey, Pierre-Marie Pédrot, Yann Régis-Gianas, Matthieu 
Sozeau, Arnaud Spiwack, Enrico Tassi with contributions also from Bruno 
Barras, Yves Bertot, Frédéric Besson, Xavier Clerc, Pierre Corbineau, 
Jean-Christophe Filliâtre, Julien Forest, Sébastien Hinderer, Assia Mahboubi, 
Guillaume Melquiond, Jean-Marc Notin, François Ripault, Carst Tankink as well 
as many external contributors.

The Coq Development Team