coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Modules within modules, Jevgenijs Sallinens
- Re: [Coq-Club] Modules within modules, Thery Laurent
- <Possible follow-ups>
- Re: [Coq-Club] Modules within modules, Jevgenijs Sallinens
Archive powered by MhonArc 2.6.16.