The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Hi everybody,
I want to know how can we re-use tactics defined inside modules ?!
Importing these modules doesn't always work as we can see clearly in 
this simple example:

Module Type SIG.
Parameter X:Set.
End SIG.

Module func[S:SIG].
Import S.
Inductive def:X ->Set:=
d:(a:X) (def a).

Tactic Definition tac:=Constructor 1.

End func.

Module sigImpl <:SIG.
Definition X:=nat.
End sigImpl.

Module func1:=func sigImpl.

Import func1.
Definition essai:(a:nat) (def a).
tac.

Here we get this error :-(  : the reference tac was not found in the 
current environment!

This seems to me strange, because it's not the case while defining a 
tactic inside a simple Module (instead of a functor) as we can see below:

Module mod.

Tactic Definition tac:=Auto.

End mod.

Import mod.

Definition ess:O=O.

tac.

Defined.



Can anyone explain this to me!

Thanks for help
Houda