The Coq mailing list

[Julien Tesson <tesson.julien AT free.fr>]

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