coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "Transparent" module types, ala O'Caml?

From: frank maltman <frank.maltman AT googlemail.com>
To: Mathieu Boespflug <mboes AT tweag.net>, <coq-club AT inria.fr>
Subject: Re: [Coq-Club] "Transparent" module types, ala O'Caml?
Date: Sun, 5 Jun 2011 20:53:13 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=date:from:to:subject:message-id:in-reply-to:references:x-mailer :mime-version:content-type:content-transfer-encoding; b=n8emCsqeZJRWLG0DcLi1S8R7ehBqljXUDTWAzYZwm5HKtHaBo7LlofxwnApedhiDvH WN8z/iEmrhLjkzKmaOETGpfctStPbvP3sB3DXF2IoWKXSqJChSyxLnKWzNj8sfMSBwi8 vxLor8NgadArCqU4GUtstnwnvNwtSZupC8IAk=

On Sun, 5 Jun 2011 16:45:58 -0400
Mathieu Boespflug
<mboes AT tweag.net>
wrote:
> Hi Frank,
>
> changing
>
> > Module Monad_Option : Base.
>
> to
>
> > Module Monad_Option <: Base.
>
> does the trick. The former masks the computational content of the
> module, while the latter just asks Coq to check that the signature of
> Monad_Option is a subtype of the signature Base.

Thank you!

[Coq-Club] "Transparent" module types, ala O'Caml?, frank maltman
- Re: [Coq-Club] "Transparent" module types, ala O'Caml?, Mathieu Boespflug
  - Re: [Coq-Club] "Transparent" module types, ala O'Caml?, frank maltman
- Re: [Coq-Club] "Transparent" module types, ala O'Caml?, AUGER Cedric
  - Re: [Coq-Club] "Transparent" module types, ala O'Caml?, Damien Pous
  - Re: [Coq-Club] "Transparent" module types, ala O'Caml?, frank maltman