coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Houda Anoun <anoun AT labri.fr>
- To: Coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] How can we use tactics defined inside modules ?!
- Date: Mon, 29 Sep 2003 12:08:51 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] How can we use tactics defined inside modules ?!, Houda Anoun
Archive powered by MhonArc 2.6.16.