diff --git a/theories/base.v b/theories/base.v
index 2b00af030f368b8bc024e982db668fed82ae1be1..8e2f922f819630feff7e4fc0d2bd60441e552b8f 100644
--- a/theories/base.v
+++ b/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.