Pattern matching notation for monadic binds

This gets rid of the old hack to have specific notations for pairs up to a fixed arity, and moreover allows to do fancy things like:

Record test := Test { t1 : nat; t2 : nat }.

Definition foo (x : option test) : option nat :=
  ''(Test a1 a2) ← x;
  Some a1.

There are some problems, however:

• It conflicts with Coq's notation ' x for Zpos x. Fortunately, the breakage is in the right direction: the proposed monadic notation breaks Coq's ' x. Furthermore, I believe said notation should be removed from Coq, see https://github.com/coq/coq/pull/6155
• It breaks backwards compatibility. Since Coq only allows to use binders in recursive notations, the notation must start with at least one symbol, for which I picked '. As such, this means we need a double '.

changed the description

Maybe https://github.com/coq/coq/pull/982 will allow us to get rid of the double tick. If so, let's postpone this.

Maybe https://github.com/coq/coq/pull/982 will allow us to get rid of the double tick.

How that?

How that?

Take a look at Hugo's example:

Parameter myex : forall {A}, (A -> Prop) -> Prop.
Notation "'myexists' x , p" := (myex (fun x => p))
  (at level 200, x pattern, p at level 200, right associativity).
Check myexists (x,y), x>y.

So, If I understand well, pattern is for a single binder, and the ' is not part of its syntax. So, if we use:

Notation "' x ← y ; z" := (y ≫= (λ x, z))
  (at level 100, x pattern, only parsing, right associativity) : stdpp_scope.

Things should work out.

Ah, the new pattern class. I see.

added 7 commits

• 4a10a9e6...376dff25 - 6 commits from branch master
• dcd59f13 - Pattern matching notation for monadic binds.

Compare with previous version

With help of Hugo Herbelin in https://github.com/coq/coq/pull/6155 I managed to make it compatible with Coq's '_ notation.

The question remaining is whether we want to merge this now, or wait until we get pattern in Coq and can get rid of the double tick.

I don't really care.

Do we have a user that would significantly benefit from having this now, but then changing it again later?

Do we have a user that would significantly benefit from having this now

Not really. I quite liked the notation in Mtac2 (and there we have quite some uses of it), so I wanted to also put it in std++.

Well, I stick with "don't care" then. If you think is is nice, and you will fix the fallout (if any) in all our reverse dependencies, it's fine for me.

Yes, I can take care of the fallout in our reverse dependencies.

mentioned in commit 5912d750

merged