Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


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





Archive powered by MhonArc 2.6.16.

Top of Page