The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

On Mon, 6 Jun 2011 10:04:23 +0200
AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:
>
> If I am not mistaken, you should have RTFM, since this part has a
> correct documentation unlike many coq features.
> 
> Module Monad_option: Base
> with Definition M := option.
> …
> End Monad_option.
> 
> should have done the trick in the OCaml way.
> 
> In a way it is better than the <:, since it abstracts exactly the parts
> you want.

Unfortunately, the wording in the manual isn't exactly ideal. It mentions
transparency only once:

"If we just want to be sure that the our implementation satisfies a
given module type without restricting the interface, we can use a
transparent constraint"

I'm not even sure what "restricting the interface" means.

The sentence on using 'with Definition', as shown above, reads:

"Now we can create a new module from M, giving it a less precise
specification: the y component is dropped as well as the body of x."

I'm not claiming it's undocumented, but it's difficult to infer the
desired behaviour from those two sentences if you're not already
familiar with the system!