Monad: Allow patterns in 'let*' notation

[Lysxia]

Closes #97

This actually reverts and improves a change in #99 (i.e., the ability to add type signatures in bindings was also removed from let*; this PR adds it back, in a terser fashion).

I think the main thing left in that issue to resolve was:

Should we remove `let* notation (which has 0 users) as well?

And I don't think so.

• It was only just added.

• IMO let* _ := _ in _ is much nicer to the point that I would recommend always using this style.

• Maybe it clashes with a Scheme convention, but OCaml gives a precedent for this notation. And in PLT "let" is in fact closely related to monads.

If I am guessing correctly, the notation _ <- _ ;; _ comes from trying to emulate Haskell's do-notation, but a crucial difference is that in Haskell it is a much less ambiguous syntax because it is announced by a do keyword and delimited by layout or braces. In Coq, those benefits don't apply so it doesn't work quite as well.

[lthms]

Should we remove `let* notation (which has 0 users) as well?

FTR, I am using it :p.

Thanks for this change @Lysxia, I was about to propose a similar one, so that’s great!