The Coq mailing list

["Carlos.SIMPSON" <carlos AT math1.unice.fr>]

Hi. It seems to me that two distinct things are going on here:
one wants to do a tactic which depends on P : T -> Prop,
for which it would suffice to have a tactic denoted
ForSome P .
On the other hand, one also wants to give a name to the variable.
It is actually possible to use fresh names in user-defined tactics,
for example

Tactic Definition Mylettac u v :=
LetTac u := v .
Here u is a fresh name whereas v should be an existing object or
a valid expression preceded by a ` .

Thus one could define a tactic whose format would be

ForSome t `P.

One could of course write this as
ForSome t `[x:_](P x)
and one imagines that probably
ForSome t `[t:_](P t)
wouldn't produce an error.
In the expression
ForSome t `(P t)
Coq wouldn't know that the second t was introduced in the first part (as
Hugo said),
or to put this differently, the expressions separated by spaces in a
tactic definition (and
marked by a ` ) have to be standalone coq expressions whereas (P t) is
not such if t doesn't already
exist. Perhaps grammar could take it from here?

---Carlos Simpson