From f4718436681da181951e4b15fc7ff1b682b4114d Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Thu, 25 Jun 2020 07:08:43 +0200
Subject: [PATCH] Fix #70: add pattern variant of bind notation

Use that in place of the old encoding:
https://gitlab.mpi-sws.org/iris/stdpp/-/issues/70#note_52817

Requires dropping support for Coq 8.7.
---
 theories/base.v      | 5 ++---
 theories/gmultiset.v | 2 +-
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 441535f8..c0ff4f96 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1046,9 +1046,8 @@ Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
 Notation "x ← y ; z" := (y ≫= (λ x : _, z))
   (at level 20, y at level 100, z at level 200, only parsing) : stdpp_scope.
 
-Notation "' x1 .. xn ← y ; z" := (y ≫= (λ x1, .. (λ xn, z) .. ))
-  (at level 20, x1 binder, xn binder, y at level 100, z at level 200,
-   only parsing, right associativity) : stdpp_scope.
+Notation "' x ← y ; z" := (y ≫= (λ x : _, z))
+  (at level 20, x pattern, y at level 100, z at level 200, only parsing) : stdpp_scope.
 
 Infix "<$>" := fmap (at level 61, left associativity) : stdpp_scope.
 
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 736980c1..fda93e2a 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -28,7 +28,7 @@ Section definitions.
     multiplicity x X = multiplicity x Y.
 
   Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X,
-    let (X) := X in ''(x,n) ← map_to_list X; replicate (S n) x.
+    let (X) := X in '(x,n) ← map_to_list X; replicate (S n) x.
   Global Instance gmultiset_size : Size (gmultiset A) := length ∘ elements.
 
   Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet ∅.
-- 
GitLab