Add the let* monadic notation

[lthms]

Closes #95

Inspired by the notation introduced by OCaml 4.08, we propose to
introduce a new notation following the same principle.

    let* x := p in q

is strictly equivalent to

    x <- p;; q

[liyishuai]

For compatibility, please create a separate module (e.g. MonadLetNotation), so that importing MonadNotation doesn't introduce two styles of notations at the same time.

[lthms]

Sorry, I misunderstood your comment on the issue.

I was not sure how to proceed, so I propose two approach:

• Always load _ <- _ ;; _, and load let* _ := _ in _ if desired (first commit)
• Load either one or the other (second commit)

I personally prefer the latter, and it does not break the previous interface afaict. What do you think?

[liyishuai]

Thanks! The latter with MonadBaseNotation looks better. I'll try to figure out how to make CI happy.

[lthms]

The failure with the CI was due to a commit I had added which was breaking old Coq version (declaring the scope). I have removed it and now it appears that it works fine.

I should probably squash the two commits together if you prefer the approach with the base module (I do too! (: ). I think it would probably be wise to add some kind of test case too, right?

[liyishuai]

Yes we could add some Notation.v under /examples.

[lthms]

I think we are good to go now!