coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [ANN] Ssreflect/MathComp 1.6.1 released

From: Ilya Sergey <i.sergey AT ucl.ac.uk>
To: coq-club AT inria.fr, ssreflect AT msr-inria.inria.fr
Subject: Re: [Coq-Club] [ANN] Ssreflect/MathComp 1.6.1 released
Date: Wed, 21 Dec 2016 17:21:24 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=i.sergey AT ucl.ac.uk; spf=None smtp.mailfrom=i.sergey AT ucl.ac.uk; spf=Pass smtp.helo=postmaster AT EUR01-VE1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:w+xHIR1WyRFHBJInsmDT+DRfVm0co7zxezQtwd8ZseISL/ad9pjvdHbS+e9qxAeQG96KsLQU0aGG7ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMijexe7B/IAu5oQjStsQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1iikIKiQ5/XnYhcx+jq1VoByvqR9izYDKfI6VNeFzcbnBcd4AX2dNQtpdWi5HD4ihb4UPFe0BPeNAoof+o1sPrQGxDhSxCuzx0D9IiWH53K0n2OkmEAHKxhcgEMwUsHTbstr0NLwfUf2pw6nM1znMde9Z1S3g6IjLax0sp+yHU7x3ccrU00YvFgXFg02fqYzkIzOV1vkNvHOB4+phUuKjk2EnqwBtojiv28cjkZPFiZ4SylDB8yhy3YU7JcWgRUJmfdKpH4Fcui6YOodsX88uWWVltDoixrEYpZK2eDIGxZcnyhLFdfCLbYaF7gj+WOuSPzt1gm9udqiliBao60egz/XxVsmq31ZOqSpIitbCuX4R2RDP98SLU/Ry8Ei81TqW0ADc8f9LLVozlarGN54u2bkwlocVsUveBCP2gF/2jKiKdko65ueo9+XnYrLgppOGMI90lx3+MqApmsy4AuQ0KBQBX2+e+eik1b3j+1P2QKlSg/ErjqXUv4rWKMsZq6KjHgNZyIIu5wqnAzejytsYnH0HLFxfeBKAiojkI1DOLOrjDfihmVSsnylkxvDdM738HprNKmLPn639crpn9k5cyxI/zcpD6JJMFrEBPPXzV1ftu9zfFx81KhC7w+L6CNpmzY4eQmKOAqqBMKzIq1OI5+QvI/ONZIAPojr9JeIltLbSiioynkZYdq2017MWbmq5F7JoOQHRemH2j9kFHGwWlg8lVqnrjkeDWHhSYWyzVuQy/GIVEoWjWKbHV4nlu7Gb0yqqVslXIHtLEF+BAF/1fIHCUvxKdSHEcZwpqSANSbX0E9xp7hqprgKvk7c=
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Hi Enrico,

Thanks a lot for the update!

One thing: at the moment math-comp, when building with the new Coq 8.6, complains a lot about deprecated Vernacular commands, such as Arguments Scope, as well about overloaded notations when importing ssrnat (e.g., "Warning: Notation _ < _ <= _ was already used in scope nat_scope").

Is there an simple workaround to suppress them?

Cheers.

Ilya

On Wed, Dec 21, 2016 at 3:19 PM Enrico Tassi <enrico.tassi AT inria.fr> wrote:

We are proud to announce the immediate availability of the
Ssreflect proof language and the Mathematical Components library
version 1.6.1 for Coq 8.4pl6, 8.5pl3 and 8.6.0.

This minor release adds compatibility with Coq 8.6 and
fixes a few bugs of the proof language related to type classes,
universe polymorphism and primitive projections. Theory files
did not change.

A detailed ChangeLog is available at:
https://github.com/math-comp/math-comp/blob/release/1.6/ChangeLog

The source archive and OPAM packages are available at the time of
writing. Windows packages will follow. Download at:
http://math-comp.github.io/math-comp/

Best regards,
--
The Mathematical Components team

[Coq-Club] [ANN] Ssreflect/MathComp 1.6.1 released, Enrico Tassi, 12/21/2016
- Re: [Coq-Club] [ANN] Ssreflect/MathComp 1.6.1 released, Ilya Sergey, 12/21/2016