coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "George Necula" <necula AT eecs.berkeley.edu>
- To: "Hugo Herbelin" <hugo.herbelin AT inria.fr>
- Cc: <coq-club AT pauillac.inria.fr>
- Subject: RE: [Coq-Club]Tactics inside functors
- Date: Tue, 31 Oct 2006 10:45:31 -0800
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
>
>
>
>
- [Coq-Club]Tactics inside functors, George Necula
- Re: [Coq-Club]Tactics inside functors,
Hugo Herbelin
- RE: [Coq-Club]Tactics inside functors, George Necula
- Re: [Coq-Club]Tactics inside functors,
Hugo Herbelin
Archive powered by MhonArc 2.6.16.