Subject: Ssreflect Users Discussion List
List archive
- 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
- [ssreflect] [ANN] Ssreflect/MathComp 1.6.1 released, Enrico Tassi, 12/21/2016
- Re: [ssreflect] [Coq-Club] [ANN] Ssreflect/MathComp 1.6.1 released, Ilya Sergey, 12/21/2016
- Re: [ssreflect] [Coq-Club] [ANN] Ssreflect/MathComp 1.6.1 released, Enrico Tassi, 12/21/2016
- Re: [ssreflect] [Coq-Club] [ANN] Ssreflect/MathComp 1.6.1 released, Maxime Dénès, 12/21/2016
- Re: [ssreflect] [Coq-Club] [ANN] Ssreflect/MathComp 1.6.1 released, Enrico Tassi, 12/21/2016
- Re: [ssreflect] [Coq-Club] [ANN] Ssreflect/MathComp 1.6.1 released, Ilya Sergey, 12/21/2016
Archive powered by MHonArc 2.6.18.