Skip to Content.
Sympa Menu

coq-club - [Coq-Club] How can we use tactics defined inside modules ?!

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How can we use tactics defined inside modules ?!


chronological Thread 
  • 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






Archive powered by MhonArc 2.6.16.

Top of Page