The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hi, 

Many (most?) Linux distributions are fairly slow as it comes to updating Coq. 
On Linux, regardless of the concrete distribution, I suggest installing Coq 
via opam. This makes it very easy to install ssreflect/mathcomp, many user 
contributions as well as multiple versions of Coq.

Best,
Christian


On 12/01/2017 09:52 PM, Michel Levy wrote:
> Thank you Gaëtan, I am still running Coq 8.4 an old version, but the last 
> version of my system Ubuntu 16.04LTS.
> 
> 
> Le 01/12/2017 à 21:42, Gaëtan Gilbert a écrit :
>> You appear to be running an older version of Coq, the definition you got 
>> from the doc is as of Coq 8.7, the other is the previous definition.
>> See https://github.com/coq/coq/pull/1017
>>
>> Gaëtan Gilbert
>>
>> On 01/12/2017 21:38, Michel Levy wrote:
>>> In the doc, Standard Library, I read the good definition
>>>
>>> Ltac classical_right := match goal with
>>> |- ?X \/ _ => elim (classic X);intro;[left;trivial|right]
>>> end.
>>>
>>> But, after "Require Import Classical", when I execute
>>>
>>> Print Ltac_classical_right
>>>
>>> I read the following definition
>>>
>>> Ltac classical_right :=
>>>    match goal with
>>>    | _:_ |- ?X1 \/ _ => elim (classic X1); intro; [ left; trivial | right 
>>> ]
>>>    end.
>>>
>>> which seems to me incorrect. Am I right or wrong ?
>>>
>>>
>>> -- 
>>> courriel : 
>>> michel.levy1948 AT gmail.com
>>> membres-liglab.imag.fr/michel.levy 
>>> <http://membres-liglab.imag.fr/michel.levy>
> 
> -- 
> courriel : 
> michel.levy1948 AT gmail.com
> membres-liglab.imag.fr/michel.levy 
> <http://membres-liglab.imag.fr/michel.levy>