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: Enrico Tassi <>
  • To:
  • Subject: Re: [ssreflect] [Coq-Club] [ANN] Ssreflect/MathComp 1.6.1 released
  • Date: Wed, 21 Dec 2016 20:11:27 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=None ; spf=None
  • Ironport-phdr: 9a23:nYGjjRTRBw8XVC0b+i7nnHdeltpsv+yvbD5Q0YIujvd0So/mwa67bBCN2/xhgRfzUJnB7Loc0qyN4vumCTZLuM7f+DBaKdoXCE9D0Z1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/hKiO/MjIeB9Fij6waq9aKQ6s6ATXrMgfx4pkMKc4jBXT8VVSfOED6GVyJFmU1yr1/dyxtMpu9T5RsPVn68dbSqTSfqIiTLUeAi5wYDN939HiqRSWFVjH3XAbSGhDyhc=

On Wed, Dec 21, 2016 at 05:21:24PM +0000, Ilya Sergey wrote:
> 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?

Unfortunately not. We should really update the theory files...

Best,
--
Enrico Tassi



Archive powered by MHonArc 2.6.18.

Top of Page