The Coq mailing list

["George Necula" <necula AT eecs.berkeley.edu>]

 If I understand correctly I have to put the definition of the tactic in
the module type. I thought that there was some way to put only a
declaration of the tactic. Anyway, this is good enough for my purposes. 

 Thank you for your help,
George.  

> -----Original Message-----
> From: Hugo Herbelin 
> [mailto:hugo.herbelin AT inria.fr]
>  
> Sent: Tuesday, October 31, 2006 9:07 AM
> To: George Necula
> Cc: 
> coq-club AT pauillac.inria.fr
> Subject: Re: [Coq-Club]Tactics inside functors
> 
> 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
> 
> 
> 
>