coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Julien Tesson <tesson.julien AT free.fr>
- To: Mailing list Coq <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] name of term in tactics
- Date: Sat, 27 Sep 2008 18:40:11 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
Is there a convenient way to re-use the name of a term in tactics definition ?
here is an example of what I'd like to do :
Ltac elim_ex e:=
repeat (
match (type of e) with
| exists x,_ =>
elim e;clear e; let H:=fresh "x" in intros H e
| _ => fail
end
).
I'd like to replace "x" with something that give me the name of the subterm x in the matched term, is it possible ?
Thanks in advance,
Julien.
begin:vcard fn:Julien Tesson n:Tesson;Julien org;quoted-printable:Laboratoire d'Informatique Fondamentale d'Orl=C3=A9ans adr:;;;;;;France email;internet:tesson.julien AT free.fr title:Doctorant tel;work:+33/(0) 2 38 41 72 68 tel;fax:+33/(0) 9 55 33 36 68 x-mozilla-html:TRUE url:http://tesson.julien.free.fr/ version:2.1 end:vcard
- [Coq-Club] name of term in tactics, Julien Tesson
- Re: [Coq-Club] name of term in tactics, Stéphane Lescuyer
Archive powered by MhonArc 2.6.16.