diff --git a/theories/base.v b/theories/base.v
index cf7f74c5228ec35d4922c4c3e895882e929a3d01..a9c3cfdddc15212da0eb3876706247e2976f7871 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -407,15 +407,18 @@ Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope.
 Notation "x ← y ; z" := (y ≫= (λ x : _, z))
   (at level 65, next at level 35, only parsing, right associativity) : C_scope.
 Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
-Notation "'( x1 , x2 ) ← y ; z" :=
+Notation "' ( x1 , x2 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1, x2) := x in z))
   (at level 65, next at level 35, only parsing, right associativity) : C_scope.
-Notation "'( x1 , x2 , x3 ) ← y ; z" :=
+Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3) := x in z))
   (at level 65, next at level 35, only parsing, right associativity) : C_scope.
-Notation "'( x1 , x2 , x3  , x4 ) ← y ; z" :=
+Notation "' ( x1 , x2 , x3  , x4 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3,x4) := x in z))
   (at level 65, next at level 35, only parsing, right associativity) : C_scope.
+Notation "' ( x1 , x2 , x3  , x4 , x5 ) ← y ; z" :=
+  (y ≫= (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
+  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
 
 Class MGuard (M : Type → Type) :=
   mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.