The Coq mailing list

[Bas Spitters <spitters AT cs.kun.nl>]

Dear Coq-users.

I want to define a "for some" tactic, which should do the following:
    For_Some t (P t)
introduces a new variable t and adds (P t) as an hypothesis.
When I do this naively:
 Assert ( EX t | (P t));Pick t.    [Pick is a previously defined tactic].

and I try For_Some t '(P t)  coq complains that t was not defined.

So, maybe, I should try doing something like For_Some [t](P t) and use
pattern matching to get what I want, but apparently it is not allowed to
pass a term to a user-defined tactic.
Although, I can do this with Apply for instance.

Am I mistaken?

Thanks in advance,

Bas Spitters