Skip to Content.
Sympa Menu

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

Subject: Ssreflect Users Discussion List

List archive

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


Chronological Thread 
  • From: Ilya Sergey <>
  • To: ,
  • Subject: Re: [ssreflect] [Coq-Club] [ANN] Ssreflect/MathComp 1.6.1 released
  • Date: Wed, 21 Dec 2016 17:21:24 +0000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=None ; spf=Pass
  • Ironport-phdr: 9a23:bOOZ7RarqjTYjk9ko/xRc2r/LSx+4OfEezUN459isYplN5qZpsWybnLW6fgltlLVR4KTs6sC0LuN9fC6EjxdqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2a3IyL0LW5/ISWaAFVjhK8Z6lzJVO4t0GZrdIMjIVmJ60t4h7SuD5Jff5XzCVpI0iSllDy/JSe5plmpgVUqvtpzMNaXqjrN/A5C6dVFjsrIkgo78mtvBKFUAjZtShUaXkfjhcdW1uN1xr9RJqk6iY=
  • 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

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


Archive powered by MHonArc 2.6.18.

Top of Page