The Coq mailing list

[Damien Pous <Damien.Pous AT inria.fr>]

> 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.

It would do the job in Ocaml, it possibly does not in Coq : this would
make all other definitions opaque, which is most of the time not what
you want.
Typically, if you want to compute with this monad, you need bind,
return, fail, and so on to be transparent.

> If I am not mistaken, you should have RTFM, since this part has a
> correct documentation unlike many coq features.

please refrain from using such acronyms, please.

Best,
Damien