The Coq mailing list

["St�phane Lescuyer" <lescuyer AT lri.fr>]

Hi, you can just write

| exists x, _ => elim e; clear e; intros x e

in the 'exists' branch and this will use the x from the matched term.
It's the same as writing

| exists x, _ => destruct e as [x e]

The problem in both cases is that the tactic will fail if there is
already an object named x in the context.
Unfortunately it seems impossible to use the metavariable x as an
argument to fresh, so I cant think of a way to make it work in
general.
Maybe you could resort to passing a correct name as an argument to the tactic 
?

Stéphane L.


2008/9/27 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.
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06