The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

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