coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Michel Levy <michel.levy1948 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Module Classical, Ltac classical_right incorrect ?
Date: Fri, 1 Dec 2017 21:38:14 +0100
Authentication-results: mail3-smtp-sop.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-wr0-f169.google.com
Ironport-phdr: 9a23:sUjSXh/5uX55Y/9uRHKM819IXTAuvvDOBiVQ1KB+1eocTK2v8tzYMVDF4r011RmSAtWdtqoMotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS46tL2HV93a19HsZHgj1HQtzPOX8XIDI3Oqt0OXn3pzYYwhMzB6wf6I6eBC3pgXcso8SjJVzc/dtmjPGp3JJf6JdwmY+dgHbpAr1+srlpM0ryC9Xof90r8M=

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 ?

[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