The Coq mailing list

["Jevgenijs Sallinens" <jevgenijs AT dva.lv>]

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