Skip to Content.
Sympa Menu

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


Chronological Thread 
  • From: Maxime Dénès <>
  • To:
  • Subject: Re: [ssreflect] Install the master branch of ssreflect with coq-8.6
  • Date: Wed, 12 Jul 2017 14:13:45 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Pass ; spf=None
  • Ironport-phdr: 9a23:bl5U3R11K+kC38SMsmDT+DRfVm0co7zxezQtwd8Zse0fIvad9pjvdHbS+e9qxAeQG96KtLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q89pDXYQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb5Sqw5VDqg4qplURPklCgKPCM9/GzXlsB8iaRWqw+jqRNi2Y7ZeJybOuRwfq3dft0US2ROUclTWCNdDY2xdJcPAugbMOpEs4XwqVkDoB2jDgesHuPvzTpIi2fx06Ig3OUhEATG0xI9FNwAqnPUqszyNLwPWu2yyanH1zTDb/dN1Df48ofJfREhofSSUr1tb8XRz1cgFxjfglWes4zoJjWY3fkDvWic6upvT+Ovi2g/pgF+oziv2scsipTSiY4P1l/E8iB5zYAoLtO7UE52edGpHZpKuy2HK4d7QtkuTmNrtSog17EKpIO3cDAJxZkp3RLTdvyKfoaS7h/sSOqdOyp0iGxkdb+5mh2861KvyvfmWcmxyFtKrjRKkt3Ltn0V0xHf8M2HSvx880qiwzqP0hrc6uBAIUwtkqrbNoIhzqQ3lpoNsUTPBCn2l1vqjKOOd0Uk/Pan6/j/b7jpp5KQLZJ4hh3+P6g0mMGyAv40PhUTU2SG4ei80afs/Uz9QLVElP02lazZvYjfJcsBp665BxRY0oM55BewDjem1coXkmQZI1JDZh2HlJLlO1/UIPzgF/ewn0yskCt3x/DBJrDhGY7NLmLdn7fvebZy9VJTyBYowNBE55NUD6kBL+jpVk/wstzYFB45PBauz+bpEtUunr8ZDHmUGKKXNK7ZrXeN/fhqIu+WZYZTuTDnKvFj6eS9o2U+nAo4dLmo2JZfRPG+nu8ud0CQYH7Eh94REGIHsgc4QfeshkfUAm0bXGq7Q69pvmJzM4mhF4qWG9ig

I keep reading messages talking about this branch renaming, and
potential incompatibilities. And I don't understand a word of it.

Either I'm completely wrong (very likely) or version detection has
nothing to do with the branch name. Can you elaborate on the link you
see between the two?

Maxime.

On 07/12/2017 02:07 PM, Enrico Tassi wrote:
> 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
>



Archive powered by MHonArc 2.6.18.

Top of Page