The Coq mailing list

[Benoît Viguier <beviguier AT gmail.com>]

Hi all,

I wanted to say thank you for the addition of the syntax coloring into
the Goal and message part of CoqIde.
I love it (and also the fact that it colors the user defined notations) !

On 12/20/2016 02:00 PM, Maxime Dénès wrote:
> 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
>>>

-- 
Kind regards,

Benoît Viguier
Software Engineer - PhD Student | Cryptography & Formal Methods
Radboud University | Mercator 1, room 03.17, Toernooiveld 212
6525 EC Nijmegen, the Netherlands | www.viguier.nl

--------------------------------------------------------------------------
This message (and any attachments) is intended solely for the addressee(s)
and may contain confidential information. If you are not the addressee, do
not copy this message (and any attachments), forward or share this message
with third parties. You are requested to notify the sender immediately and
delete this message.

Attachment: signature.asc
Description: OpenPGP digital signature