diff --git a/CHANGELOG.md b/CHANGELOG.md
index a0f0854743dca1296ee203a4cf9ea604d84b666e..f65456238aba9eb2e1454ea85d0ecde18a677492 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -35,6 +35,8 @@ sarahzrf, and Tej Chajed.
   as integers `Z`, in analogy with `encode_nat`/`decode_nat`.
 - Fix list `Datatypes.length` and string `strings.length` shadowing (`length`
   should now always be `Datatypes.length`).
+- Change the notation for pattern matching monadic bind into `'pat ← x; y`. It
+  was `''pat ← x; y` (with double `'`) due to a shortcoming of Coq ≤8.7.
 
 ## std++ 1.3 (released 2020-03-18)
 
diff --git a/theories/base.v b/theories/base.v
index 441535f82f931a6442a27c2fe8a259594511991a..c0ff4f965196cef1b91e1510f19ab765b94d65c7 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 736980c18f06b4069698847bdff28e1ecdf7a982..fda93e2ae8018f6a47c5fc35e02e76869527c08b 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 ∅.