diff --git a/theories/base.v b/theories/base.v
index 9fd4a3f4175a6eaf092cd8817217357ff4198782..8f31d3e6ae04045cdeca7bb646eb8cc4c4d924f9 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1053,64 +1053,67 @@ Global Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
    recursive notation system, so we define individual notations
    for some cases relevant in practice. *)
 (* The "format" makes sure that linebreaks are placed after the separating semicola [;] when printing. *)
+(* TODO : we are using parantheses in the "de-sugaring" of the notation instead of [$] because Coq 8.12
+   and earlier have trouble with using the notation for printing otherwise.
+   Once support for Coq 8.12 is dropped, this can be replaced with [$]. *)
 Notation "{[ k1 := a1 ; k2 := a2 ]}" :=
   (<[ k1 := a1 ]>{[ k2 := a2 ]})
   (at level 1, format
   "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ']' ']' ]}") : stdpp_scope.
 Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ]}" :=
-  (<[ k1 := a1 ]> $ <[ k2 := a2 ]>{[ k3 := a3 ]})
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]>{[ k3 := a3 ]}))
   (at level 1, format
   "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ']' ']' ]}") : stdpp_scope.
 Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ]}" :=
-  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]>{[ k4 := a4 ]})
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]>{[ k4 := a4 ]})))
   (at level 1, format
   "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ']' ']' ]}") : stdpp_scope.
 Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ]}" :=
-  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]>{[ k5 := a5 ]})
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]>{[ k5 := a5 ]}))))
   (at level 1, format
   "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ']' ']' ]}") : stdpp_scope.
 Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ]}" :=
-  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
-    <[ k5 := a5 ]>{[ k6 := a6 ]})
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]>{[ k6 := a6 ]})))))
   (at level 1, format
   "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ']' ']' ]}") : stdpp_scope.
 Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ]}" :=
-  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
-    <[ k5 := a5 ]> $ <[ k6 := a6 ]>{[ k7 := a7 ]})
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]>{[ k7 := a7 ]}))))))
   (at level 1, format
   "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ']' ']' ]}") : stdpp_scope.
 Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ]}" :=
-  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
-    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]>{[ k8 := a8 ]})
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]>{[ k8 := a8 ]})))))))
   (at level 1, format
   "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ']' ']' ]}") : stdpp_scope.
 Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ]}" :=
-  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
-    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]>{[ k9 := a9 ]})
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]>{[ k9 := a9 ]}))))))))
   (at level 1, format
   "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ']' ']' ]}") : stdpp_scope.
 Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ]}" :=
-  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
-    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
-    <[ k9 := a9 ]>{[ k10 := a10 ]})
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> (
+    <[ k9 := a9 ]>{[ k10 := a10 ]})))))))))
   (at level 1, format
   "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ; ']'  '/' '[' k10  :=  a10 ']' ']' ]}") : stdpp_scope.
 Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ]}" :=
-  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
-    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
-    <[ k9 := a9 ]> $ <[ k10 := a10 ]>{[ k11 := a11 ]})
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> (
+    <[ k9 := a9 ]> ( <[ k10 := a10 ]>{[ k11 := a11 ]}))))))))))
   (at level 1, format
   "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ; ']'  '/' '[' k10  :=  a10 ; ']'  '/' '[' k11  :=  a11 ']' ']' ]}") : stdpp_scope.
 Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ; k12 := a12 ]}" :=
-  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
-    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
-    <[ k9 := a9 ]> $ <[ k10 := a10 ]> $ <[ k11 := a11 ]>{[ k12 := a12 ]})
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> (
+    <[ k9 := a9 ]> ( <[ k10 := a10 ]> ( <[ k11 := a11 ]>{[ k12 := a12 ]})))))))))))
   (at level 1, format
   "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ; ']'  '/' '[' k10  :=  a10 ; ']'  '/' '[' k11  :=  a11 ; ']'  '/' '[' k12  :=  a12 ']' ']' ]}") : stdpp_scope.
 Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ; k12 := a12 ; k13 := a13 ]}" :=
-  (<[ k1 := a1 ]> $ <[ k2 := a2 ]> $ <[ k3 := a3 ]> $ <[ k4 := a4 ]> $
-    <[ k5 := a5 ]> $ <[ k6 := a6 ]> $ <[ k7 := a7 ]> $ <[ k8 := a8 ]> $
-    <[ k9 := a9 ]> $ <[ k10 := a10 ]> $ <[ k11 := a11 ]> $ <[ k12 := a12 ]>{[ k13 := a13 ]})
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> (
+    <[ k9 := a9 ]> ( <[ k10 := a10 ]> ( <[ k11 := a11 ]> ( <[ k12 := a12 ]>{[ k13 := a13 ]}))))))))))))
   (at level 1, format
   "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ; ']'  '/' '[' k10  :=  a10 ; ']'  '/' '[' k11  :=  a11 ; ']'  '/' '[' k12  :=  a12 ; ']'  '/' '[' k13  :=  a13 ']' ']' ]}") : stdpp_scope.