Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] module question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] module question


chronological Thread 
  • From: Frederic Blanqui <Frederic.Blanqui AT loria.fr>
  • To: Houda Anoun <anoun AT labri.fr>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] module question
  • Date: Mon, 14 Feb 2005 10:29:49 +0100 (CET)
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Tue, 8 Feb 2005, Houda Anoun wrote:

Module use_multi(AT:At)(ms:Multi_Set with Module O:= (setOrd AT)).

in a "with" clause, you can only use names for modules. see http://coq.inria.fr/doc/Reference-Manual004.html#toc14.




Archive powered by MhonArc 2.6.16.

Top of Page