The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

>  I was able to use a tactic defined in a module. But if I want to
> ascribe a module type to the module, how can I declare the tactic in the
> module type? 
> 
>  Is it possible to define tactics inside functors? 

Declaring a tactic in a module type is done the same way as declaring a
tactic in a module. For instance

Module Type U.
Ltac myintro := intro.
Tactic Notation "myassumption" := assumption.
End U.

Then, there is no subtyping for tactics. So, if you ascribe a module
type to a module, only the tactics declared in the module type are
available (if a tactic with a same name exists in the module, it is
simply discarded even if the body of the tactic differs). For
instance:

Module M : U.
End M.

Goal True->True.
M.myintro.
Import M. (* to import the tactic notation *)
myassumption.
Qed.

As a consequence, I don't see how to have an explicitly typed functor
that defines a tactic dependent of a tactic defined in the argument of
the functor, if this is the question.

Best regards,

Hugo Herbelin