The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hi Ralf,

Thanks for your positive feedback :)

The Coq 8.6 OPAM package is now available, as well as the one for CoqIDE.

Enjoy!

Maxime.

On 12/16/16 21:19, Ralf Jung wrote:
> Hi all,
> 
> thanks a lot to everyone involved in this release :)
> I've already been using the 8.6 branch for some weeks now because it's
> so much faster than 8.5 (~30% speedup for us) -- this is a solid release
> indeed.
> 
> Now I'm waiting for the new version to appear in opam so that I can
> switch away from the 8.6.dev branch... ;)
> 
> Kind regards,
> Ralf
> 
> On 16.12.2016 17:29, Maxime Dénès wrote:
>> Dear Coq Clubbers,
>>
>> The Coq development team is pleased to announce the final release of Coq
>> 8.6, available at:
>>
>>   http://coq.inria.fr/download
>>
>> You may need to refresh the page if your browser has a previous version
>> in cache.
>>
>> Source, Windows and OS X packages are available.
>>
>> This release includes:
>>
>> - A new, faster state-of-the-art universe constraint checker by
>>   Jacques-Henri Jourdan.
>> - In CoqIDE and other asynchronous interfaces, more fine-grained
>>   asynchronous processing and error reporting by Enrico Tassi, making
>>   Coq capable of recovering from errors and continuing to process the
>>   document.
>> - Better access to the proof engine features from Ltac: goal management
>>   primitives, range selectors and a typeclasses eauto engine handling
>>   multiple goals and multiple successes, by Cyprien Mangin, Matthieu
>>   Sozeau and Arnaud Spiwack.
>> - Tactic behavior uniformization and specification, generalization of
>>   intro-patterns by Hugo Herbelin and others.
>> - A brand new warning system allowing to control warnings, turn them
>>   into errors or ignore them selectively by Maxime Dénès, Guillaume
>>   Melquiond, Pierre-Marie Pédrot and others.
>> - Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
>> - The ssreflect subterm selection algorithm by Georges Gonthier and
>>   Enrico Tassi, now accessible to tactic writers through the
>>   ssrmatching plugin.
>> - LtacProf, a profiler for Ltac by Jason Gross, Paul Steckler, Enrico
>>   Tassi and Tobias Tebbi.
>>
>> A short demo of some of these new features can be run in your browser,
>> thanks to Emilio Gallego's JsCoq, at:
>>
>>   https://x80.org/rhino-coq/examples/Coq86.html
>>
>> See http://coq.inria.fr/ and the CHANGES file in the distribution for
>> for more details.
>>
>> Coq 8.6 initiates a time-based release cycle, with a major version being
>> released every 10 months. The roadmap is also made public.
>>
>> To date, Coq 8.6 contains more external contributions than any previous
>> Coq version. Code reviews were systematically done before integrating
>> new features, with an important focus given to compatibility and
>> performance issues.
>>
>> The Coq Development Team
>>