The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi Maxime and coq-club,

Congratulation to everyone who contributed to this release! It's great to see 
Coq making quick progress.

Cheers,
Clément.

On 01/21/2016 07:22 PM, Maxime Dénès wrote:
> Dear Coq-Clubers,
> 
>   The Coq development team is pleased to announce the final release
> of Coq 8.5 available at:
> 
>   http://coq.inria.fr/coq-85
> 
>   This release includes many bug fixes with respect to the previous
> versions, and a few incompatible changes, see the following file for
> more information:
> 
>   https://coq.inria.fr/distrib/V8.5/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 ltac:(..) 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
> 
>

Attachment: signature.asc
Description: OpenPGP digital signature