The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Dear Coq developers,

thanks a lot for this solid release. Our developments ported over with
no effort.  I guess for Iris itself, it being in the CI, that's not so
surprising, but the Rust stuff built on top of that also needed exactly
no changes.  As a nice bonus everything got ~11% faster. :-)

Kind regards,
Ralf

On 06.09.2017 15:18, Maxime Dénès wrote:
> Dear Coq clubbers,
> 
>   The Coq development team is pleased to announce the release of the
> first beta version of Coq 8.7, available at:
> 
> http://coq.inria.fr/coq-87
> 
> Source, Windows and OS X packages are available at:
> 
> https://github.com/coq/coq/releases/tag/V8.7%2Bbeta1
> 
> This release includes:
> 
> - A large amount of work on cleaning and speeding up the code base,
> notably the work of Pierre-Marie Pédrot on making the tactic-level
> system insensitive to existential variable expansion, providing a safer
> API to plugin writers and making the code more robust.
> 
> - New tactics:
>   Variants of tactics supporting existential variables eassert, eenough,
> etc. by Hugo Herbelin;
>   Tactics extensionality in H and inversion_sigma by Jason Gross;
>   specialize with accepting partial bindings by Pierre Courtieu.
> 
> - Cumulative Polymorphic Inductive Types, allowing cumulativity of
> universes to go through applied inductive types, by Amin Timany and
> Matthieu Sozeau.
> 
> - The SSReflect plugin by Georges Gonthier, Assia Mahboubi and Enrico
> Tassi was integrated (with its documentation in the reference manual) by
> Maxime Dénès, Assia Mahboubi and Enrico Tassi.
> 
> - The coq_makefile tool was completely redesigned by Enrico Tassi to
> improve its maintainability and the extensibility of generated
> Makefiles, and to make _CoqProject files more palatable to IDEs.
> 
> A lot of other changes are described in the CHANGES file.
> 
> This is the second release of Coq developed on a time-based development
> cycle. Its development spanned 9 months from the release of Coq 8.6 and
> was based on a public road-map. It attracted many external
> contributions. Code reviews and continuous integration testing were
> systematically used before integration of new features, with an
> important focus given to compatibility and performance issues.
> 
> The Coq Development Team
> 
> 
> 
> 
> 
> 
> 
>