The Coq mailing list

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

> On Sun, 22 Feb 2004, Thery Laurent wrote:
>
> 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


I mean, it would be nice to have some possibility to keep
opaque option here.
Imagine,for example,one has published first version of module I for common
use.
Then there is no warranty that second version, with modified implementation
of
same signature, could be used as the substitute for the first one,
with no additional problems, related with the usage of undocumented
features.

Regards,
Jevgenijs.

________________________________________________
Message sent using UebiMiau 2.7.2