The Coq mailing list

[Loic Pottier <loic.pottier AT sophia.inria.fr>]

Hi,

with Ltac, can we match names of variables in a pattern, to use them in 
right-hand side? e.g:

Ltac tac:=
 match goal with
  |- forall ?x:?E, ?P => idtac x
end.

(but this does not work :-(  )

or, if not, associate a character to a type so that intro will use it by 
default?

Loïc