coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Tactics inside functors

From: "George Necula" <necula AT eecs.berkeley.edu>
To: <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club]Tactics inside functors
Date: Sat, 21 Oct 2006 19:04:18 -0700
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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?

Thanks,
George.

[Coq-Club]Tactics inside functors, George Necula
- Re: [Coq-Club]Tactics inside functors, Hugo Herbelin
  - RE: [Coq-Club]Tactics inside functors, George Necula