diff --git a/tests/notation.ref b/tests/notation.ref
index 026cb4d4e5ddced30371859d4f9504f682bc8522..4d53c67c775137daaf00f3b83ff54b17c83080ef 100644
--- a/tests/notation.ref
+++ b/tests/notation.ref
@@ -24,3 +24,12 @@ test_op_4 =
   4 := {[4 := [4]]};
   5 := {[5 := [5]]}]}
      : M (M (list nat))
+test_gmultiset_1 = {[+ 10 +]}
+     : gmultiset nat
+test_gmultiset_2 = {[+ 10; 11 +]}
+     : gmultiset nat
+test_gmultiset_3 = {[+ 10; 11; 2 - 2 +]}
+     : gmultiset nat
+test_gmultiset_4 = 
+{[+ {[+ 10 +]}; ∅; {[+ 2 - 2; 10 +]} +]}
+     : gmultiset (gmultiset nat)
diff --git a/tests/notation.v b/tests/notation.v
index 467f1952d55d74f57b84d70d17430bb78dc16053..41fe94e9cea8db3335688669f0386d3c196390a7 100644
--- a/tests/notation.v
+++ b/tests/notation.v
@@ -1,4 +1,4 @@
-From stdpp Require Import base tactics fin_maps.
+From stdpp Require Import base tactics fin_maps gmultiset.
 
 (** Test parsing of variants of [(≡)] notation. *)
 Lemma test_equiv_annot_sections `{!Equiv A, !Equivalence (≡@{A})} (x : A) :
@@ -35,3 +35,17 @@ Section map_notations.
   Print test_op_3.
   Print test_op_4.
 End map_notations.
+
+(** Test that notations for maps with multiple elements can be parsed and printed correctly. *)
+Section multiset_notations.
+  Definition test_gmultiset_1 : gmultiset nat := {[+ 10 +]}.
+  Definition test_gmultiset_2 : gmultiset nat := {[+ 10; 11 +]}.
+  Definition test_gmultiset_3 : gmultiset nat := {[+ 10; 11; 2 - 2 +]}.
+  Definition test_gmultiset_4 : gmultiset (gmultiset nat) :=
+    {[+ {[+ 10 +]}; ∅; {[+ 2 - 2; 10 +]} +]}.
+
+  Print test_gmultiset_1.
+  Print test_gmultiset_2.
+  Print test_gmultiset_3.
+  Print test_gmultiset_4.
+End multiset_notations.
\ No newline at end of file
diff --git a/theories/base.v b/theories/base.v
index be247b96e616d2a84676b9cecd9ad01c61899eb7..a0507871fb1bf0f40e62d095ce830f80b11e9e31 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -938,10 +938,11 @@ Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
 Class SingletonMS A B := singletonMS: A → B.
 Global Hint Mode SingletonMS - ! : typeclass_instances.
 Instance: Params (@singletonMS) 3 := {}.
-Notation "{[+ x +]}" := (singletonMS x) (at level 1) : stdpp_scope.
+Notation "{[+ x +]}" := (singletonMS x)
+  (at level 1, format "{[+  x  +]}") : stdpp_scope.
 Notation "{[+ x ; y ; .. ; z +]}" :=
   (disj_union .. (disj_union (singletonMS x) (singletonMS y)) .. (singletonMS z))
-  (at level 1) : stdpp_scope.
+  (at level 1, format "{[+  x ;  y ;  .. ;  z  +]}") : stdpp_scope.
 
 Definition option_to_set `{Singleton A C, Empty C} (mx : option A) : C :=
   match mx with None => ∅ | Some x => {[ x ]} end.