Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Modules within modules

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Modules within modules


chronological Thread 
  • From: "Jevgenijs Sallinens" <jevgenijs AT dva.lv>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] Modules within modules
  • Date: Sun, 22 Feb 2004 12:18:21 +0200
  • Importance: Medium
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear Coq users and developers,

I found it inconvenient that it is impossible to use modules within modules
unless they are declared in module types. Here is an example.

Module Type I_Test.
End I_Test.

Module I : I_Test.
Module M_Test.
Definition test:=O.
End M_Test.
End I.
(*Anomaly: Keep objects before substitutive. Please report.*)

Is there some possibility to introduce module like M_Test for internal usage
within module I without decalring it in the interface I_Test?

Thanks,
Jevgenijs.

________________________________________________
Message sent using UebiMiau 2.7.2





Archive powered by MhonArc 2.6.16.

Top of Page