coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Module Classical, Ltac classical_right incorrect ?

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Module Classical, Ltac classical_right incorrect ?
Date: Fri, 1 Dec 2017 21:42:24 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay2-d.mail.gandi.net
Ironport-phdr: 9a23:QEKxPRHSonFfzFSdzB0BN51GYnF86YWxBRYc798ds5kLTJ76ocuwAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TXhpQIVTx74LE9+Ivn/Mo/UlcW+ke6oqLPJZAAdqzM+fbp0Gzq3qQ/crNVe1YRrJ7o4zF3Go39Cdv5K7XhrNEmQnhP56932+pN/pXcD88k9/tJNBP2pN58zSqZVWWwr

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>

[Coq-Club] Module Classical, Ltac classical_right incorrect ?, Michel Levy, 12/01/2017
- Re: [Coq-Club] Module Classical, Ltac classical_right incorrect ?, Gaëtan Gilbert, 12/01/2017
  - Re: [Coq-Club] Module Classical, Ltac classical_right incorrect ?, Michel Levy, 12/01/2017
    - Re: [Coq-Club] Module Classical, Ltac classical_right incorrect ?, Christian Doczkal, 12/02/2017