Ralf's suggested singleton notation.

theories/base.v

@@ -866,7 +866,7 @@ Notation "{[ x ; y ; .. ; z ]}" :=
   (union .. (union (singleton x) (singleton y)) .. (singleton z))
   (at level 1) : stdpp_scope.
 
-Notation "+{[ x ; y ; .. ; z ]}" :=
+Notation "{[ x ;+ y ;+ .. ;+ z ]}" :=
   (disj_union .. (disj_union (singleton x) (singleton y)) .. (singleton z))
   (at level 1) : stdpp_scope.