The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

Hello Hugo,

> If you think this is important, we may think to do it at some further
> time.

Unfortunately, I do not think what I was attempting is such important 
that it motivates the extension ;-)

I was looking for a modular way to abstract tactics over lemmas used, 
exploiting untypedness of Ltac.
So I was on the way to see whether Tac.mytac below: 

Section Tac.

Variables p: Prop.

Ltac mytac x := generalize (p x).

End Tac.

is equivalent to "mytac p x := generalize (p x)".

Now I am experimenting to see how a similar attempt works with functors;
is there some documentation of the possible combination of Ltac and functors?

Best regards,
Keiko