The `coq-prelude`

package yet to be published to Opam propose the following notation based on the recent custom entry mechanism:

```
Declare Custom Entry monad.
Notation "'do' p 'end'" := p (p custom monad at level 10) : prelude_scope
Notation "p ';' q" := (bind p%monad (fun _ => q%monad))
(in custom monad at level 10, q at level 10, right associativity, only
parsing).
Notation "'let*' a ':=' p 'in' q" := (bind p%monad (fun a => q%monad))
(in custom monad at level 0, a ident, p constr, q at level 10, right associativity, only parsing).
Notation "'let' a ':=' p 'in' q" := (let a := p in q%monad)
(in custom monad at level 5, a ident, p constr, q at level 10, right associativity, only parsing).
Notation "x" := x%monad (in custom monad at level 0, x constr at level 200, only parsing).
```

The idea is to be very analogous to OCaml monadic let.

Basically I am the only user of this notation yet, and I would be surprised to see PG support it explicitly, but eh, it exists!