diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index 7abe015f23..8bbe6ce902 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -115,28 +115,28 @@ Reserved Notation "v [[ i ]]" (at level 30).
 Reserved Notation "u {{ i }}" (at level 30).
 Reserved Notation "a # b" (at level 55, no associativity). (* match with theories/QArith/QArith_base.v *)
 Reserved Notation "'plet' x := y 'in' z"
-         (at level 200, z at level 200, format "'plet'  x  :=  y  'in' '//' z").
+         (at level 10, z at level 200, format "'plet'  x  :=  y  'in' '//' z").
 Reserved Notation "'nlet' x := A 'in' b"
-         (at level 200, b at level 200, x at level 99, format "'nlet'  x  :=  A  'in' '//' b").
+         (at level 10, b at level 200, x at level 99, format "'nlet'  x  :=  A  'in' '//' b").
 Reserved Notation "'nlet' x : tx := A 'in' b"
-         (at level 200, b at level 200, x at level 99, format "'nlet'  x  :  tx  :=  A  'in' '//' b").
+         (at level 10, b at level 200, x at level 99, format "'nlet'  x  :  tx  :=  A  'in' '//' b").
 Reserved Notation "'slet' x .. y := A 'in' b"
-         (at level 200, x binder, y binder, b at level 200, format "'slet'  x .. y  :=  A  'in' '//' b").
+         (at level 10, x binder, y binder, b at level 200, format "'slet'  x .. y  :=  A  'in' '//' b").
 Reserved Notation "'llet' x := A 'in' b"
-         (at level 200, b at level 200, format "'llet'  x  :=  A  'in' '//' b").
+         (at level 10, b at level 200, format "'llet'  x  :=  A  'in' '//' b").
 Reserved Notation "'expr_let' x := A 'in' b"
-         (at level 200, b at level 200, format "'expr_let'  x  :=  A  'in' '//' b").
+         (at level 10, b at level 200, format "'expr_let'  x  :=  A  'in' '//' b").
 Reserved Notation "'mlet' x := A 'in' b"
-         (at level 200, b at level 200, format "'mlet'  x  :=  A  'in' '//' b").
+         (at level 10, b at level 200, format "'mlet'  x  :=  A  'in' '//' b").
 (* Note that making [Let] a keyword breaks the vernacular [Let] in Coq 8.4 *)
 Reserved Notation "'dlet_nd' x .. y := v 'in' f"
-         (at level 200, x binder, y binder, f at level 200, format "'dlet_nd'  x .. y  :=  v  'in' '//' f").
+         (at level 10, x binder, y binder, f at level 200, format "'dlet_nd'  x .. y  :=  v  'in' '//' f").
 Reserved Notation "'dlet' x .. y := v 'in' f"
-         (at level 200, x binder, y binder, f at level 200, format "'dlet'  x .. y  :=  v  'in' '//' f").
+         (at level 10, x binder, y binder, f at level 200, format "'dlet'  x .. y  :=  v  'in' '//' f").
 Reserved Notation "'pflet' x , pf := y 'in' f"
-         (at level 200, f at level 200, format "'pflet'  x ,  pf  :=  y  'in' '//' f").
-Reserved Notation "'λ' x .. y , t" (at level 200, x binder, y binder, right associativity, format "'λ'  x .. y , '//' t").
-Reserved Notation "'λn'  x .. y , t" (at level 200, right associativity).
+         (at level 10, f at level 200, format "'pflet'  x ,  pf  :=  y  'in' '//' f").
+Reserved Notation "'λ' x .. y , t" (at level 10, x binder, y binder, t at level 200, format "'λ'  x .. y , '//' t").
+Reserved Notation "'λn'  x .. y , t" (at level 10, t at level 200).
 Reserved Notation "x ::> ( max_bitwidth = v )"
          (at level 70, no associativity, format "x  ::>  ( max_bitwidth  =  v )").
 Reserved Notation "r[ l ~> u ]" (l at level 69, format "r[ l  ~>  u ]").
@@ -170,7 +170,7 @@ Reserved Notation "## x" (at level 9, x at level 9, format "## x").
 Reserved Notation "### x" (at level 9, x at level 9, format "### x").
 Reserved Notation "#### x" (at level 9, x at level 9, format "#### x").
 Reserved Notation "##### x" (at level 9, x at level 9, format "##### x").
-Reserved Notation "\ x .. y , t" (at level 200, x binder, y binder, right associativity, format "\  x .. y , '//' t").
+Reserved Notation "\ x .. y , t" (at level 10, x binder, y binder, t at level 200, format "\  x .. y , '//' t").
 
 (* TODO: Remove these when https://github.com/mit-plv/bbv/pull/13 is merged *)
 Reserved Notation "# x" (at level 0, format "# x").