Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Michel Levy <michel.levy1948 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Module Classical, Ltac classical_right incorrect ?
  • Date: Fri, 1 Dec 2017 21:52:26 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michel.levy1948 AT gmail.com; spf=Pass smtp.mailfrom=michel.levy1948 AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f50.google.com
  • Ironport-phdr: 9a23:sqKxmB1M7NPyti8ssmDT+DRfVm0co7zxezQtwd8ZsesQKvad9pjvdHbS+e9qxAeQG96Eu7QZ06L/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tLw6annrn5jkLXx77KABdJ+LvG4eUgd7k+fq1/sj2Yg5IiT71Rb5sPV3iqATatsQSx49vNLdom0eZinRNcuVSg2hvIATAzF7H+s6s8cs7oGxrsPU7+psYXA==

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>


Archive powered by MHonArc 2.6.18.

Top of Page