The Coq mailing list

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

Hello.

I am looking for a way to control name-space of my own tactics;
I want to hide auxiliary Ltac functions from the outside,
but export only interesting ones.

I know that I can define tactics in a module type, 
but I have not way to define them
without mentioning, thus exporting, auxiliaries. 

With best regards,
Keiko