ssreflect - Re: [ssreflect] Install the master branch of ssreflect with coq-8.6

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Install the master branch of ssreflect with coq-8.6

From: Enrico Tassi <>
To:
Subject: Re: [ssreflect] Install the master branch of ssreflect with coq-8.6
Date: Wed, 12 Jul 2017 14:07:16 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=None ; spf=None
Ironport-phdr: 9a23:NnuEwxdQxPFPPOfMU0SNBWrVlGMj4u6mDksu8pMizoh2WeGdxcu+bR7h7PlgxGXEQZ/co6odzbGH7Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9GiTe5Y75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM3/mHZhNJtgqxYrhKuqABwzJPWb46bL/d+Yr/RcMkGSWZdRMtdSSpMCZ68YYsVCOoBOP5VoYb7p1sUrBuxGQ6sD/7xxDBSnX/2xqw62PkmHA7Y2gwgBdMOv2jTrNnvKKcdS/u1zLLJzTjYbvNW3y396InSfRw7r/GMR6t9fMzMwkchEAPFi0+fqY3jPz6N2eQNsnSb7+p9Ve20kWIotwZxoj2py8wxiYfJnpoYx1TL+Clj3oo4K8e0RU9/bNK+DZdcqSOXO5NrTs4sQGxkoiI3x7wctZKlYCQG1I4ryh7eZvGBboOG+AjsVPyLLjd9nH9leKywhxK18UW4xO3zSNW00EpXripDjtnDrGoB1xvJ6siIUvd9/0Gh1iiT1w3L7uxJLlo4mbTVJpI7w7M9koAfvVndEiL0gEn2ibWZdkQg+uim8eTnZbDmq4eTN4BukAHxLL8ul9exAesmLggOQ3Wb+eKg1LL550H5R69KjvIunqnDrJ/aPdgbprK+AwJNyYYj8Ay/ACmo0NQcg3YIME5FdQmcj4npPlHOOOr3Ae2+g1SqijdrxurJMqfvApXXfTD/l+L6Zqxw5UpRwxYbyMtFopNSELAIZvP1QE748tLCXTEjNAnh7uD9Cd56nr8XQnmOSvuUNrnTuljO+us0OOikZYkPuT+7JeJztK2mtmMwhVJIJfrh5pAQcn3tRvk=

On Wed, Jul 12, 2017 at 01:18:55PM +0200, Yves Bertot wrote:
> I tried reverting to an older version of mathcomp, but my first tries
> failed too, because I was not able to find the right
> one. Will somebody advise me as to the bets strategy to follow?

I'd like you to fix this file in you local checkout of MathComp and
retry:

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/Makefile.detect-coq-version

As you can see line 1 greps for trunk, while Coq's master branch is now
called "master". I don't know if it will be sufficient, but may explain
why it fails to detect correctly which version of Coq you are using and
consequently assume that the plugin is part of Coq (or not).

Ciao
--
Enrico Tassi

[ssreflect] Install the master branch of ssreflect with coq-8.6, Yves Bertot, 07/12/2017
- Re: [ssreflect] Install the master branch of ssreflect with coq-8.6, Enrico Tassi, 07/12/2017
  - Re: [ssreflect] Install the master branch of ssreflect with coq-8.6, Maxime Dénès, 07/12/2017
    - Re: [ssreflect] Install the master branch of ssreflect with coq-8.6, Enrico Tassi, 07/12/2017
      - Re: [ssreflect] Install the master branch of ssreflect with coq-8.6, Maxime Dénès, 07/12/2017
        
        Re: [ssreflect] Install the master branch of ssreflect with coq-8.6, Enrico Tassi, 07/12/2017
        
        Re: [ssreflect] Install the master branch of ssreflect with coq-8.6, Yves Bertot, 07/12/2017
        
        Re: [ssreflect] Install the master branch of ssreflect with coq-8.6, Enrico Tassi, 07/12/2017
        Re: [ssreflect] Install the master branch of ssreflect with coq-8.6, Yves Bertot, 07/13/2017
        Re: [ssreflect] Install the master branch of ssreflect with coq-8.6, Enrico Tassi, 07/13/2017
        Re: [ssreflect] Install the master branch of ssreflect with coq-8.6, Maxime Dénès, 07/13/2017
        
        Message not available
        Re: [ssreflect] Install the master branch of ssreflect with coq-8.6, Yves Bertot, 07/13/2017

List archive

Re: [ssreflect] Install the master branch of ssreflect with coq-8.6