Skip to Content.
Sympa Menu

coq-club - [Coq-Club] name of term in tactics

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] name of term in tactics


chronological Thread 
  • 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




Archive powered by MhonArc 2.6.16.

Top of Page