coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Hugo Herbelin <herbelin AT pauillac.inria.fr>
To: anoun AT labri.fr
Cc: Coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] How can we use tactics defined inside modules ?!
Date: Mon, 29 Sep 2003 12:22:31 +0200 (MET DST)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

  Hi,

> I want to know how can we re-use tactics defined inside modules ?!

  I guess you're working in version 7.4. Tactic definitions are
unfortunately not compatible with module imports in this version. You
have to wait for the next version (version 8) of Coq (or get the
anonymous cvs version and call coqtop with option -v7).

  Best regards.

  Hugo Herbelin

[Coq-Club] How can we use tactics defined inside modules ?!, Houda Anoun
- Re: [Coq-Club] How can we use tactics defined inside modules ?!, Hugo Herbelin