The Coq mailing list

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

Dear Coq users,

I would like to write my own tactical with a variable number of arguments.
Like Intros: we can use Intros, but also Intros a b.

How would I do this?

A related question.
I would like to make a tactical existing of several words.
Like Unfold: Unfold x in H.

How would I do this?

Thanks in advance,

Bas Spitters