coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Thery Laurent <thery AT ns.di.univaq.it>
- To: Jevgenijs Sallinens <jevgenijs AT dva.lv>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Modules within modules
- Date: Sun, 22 Feb 2004 18:28:59 +0100 (CET)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Sun, 22 Feb 2004, Jevgenijs Sallinens wrote:
>
> 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.*)
I think it is the idea of the notation <: to let modules be
bigger than their signature. If you write:
Module I <: I_Test.
Module M_Test.
Definition test:=O.
End M_Test.
End I.
everything works fine
--Laurent
- [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.