The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Dear all,

I am wondering if there is a way to define macros within the
tactic language.

For instance, consider that I have already defined
tactic notations such as:

wcbv step
wcbv iter <integer>
wcbv hyp
wcbv trans <uconstr>

Then I would like to be able to write

wcbv step, hyp, hyp, trans (t @ a), iter 2.

instead of

wcbv step; do 2 wcbv hyp; wcbv trans (t @ a); wcbv iter 2.

Can I do this using Ltac and Tactic Notation ?
Because it seems neither can input <text> as an
argument (like latex or metapost macros would do)

Thanks very much in advance for any hint

Dominique