diff --git a/coq-iris.opam b/coq-iris.opam
index b1b16597266ad2f5d0cb41888e0b4286eeb383fd..6c1f4a374559cabfab6c4c4f364231d81c8f8b26 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -14,7 +14,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo
 
 depends: [
   "coq" { (>= "8.12" & < "8.14~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2021-04-08.1.5843163b") | (= "dev") }
+  "coq-stdpp" { (= "dev.2021-04-20.2.03290b88") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index a56da2ac8c8aee78070c5859a970549cf29407f6..b0f38ffbf7814864f9dc6356c523a4750b417882 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -630,13 +630,13 @@ Section gmultiset.
     ([^o mset] y ∈ X ⊎ Y, f y) ≡ ([^o mset] y ∈ X, f y) `o` [^o mset] y ∈ Y, f y.
   Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_disj_union big_opL_app. Qed.
 
-  Lemma big_opMS_singleton f x : ([^o mset] y ∈ {[ x ]}, f y) ≡ f x.
+  Lemma big_opMS_singleton f x : ([^o mset] y ∈ {[+ x +]}, f y) ≡ f x.
   Proof.
     intros. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_singleton /= right_id.
   Qed.
 
   Lemma big_opMS_delete f X x :
-    x ∈ X → ([^o mset] y ∈ X, f y) ≡ f x `o` [^o mset] y ∈ X ∖ {[ x ]}, f y.
+    x ∈ X → ([^o mset] y ∈ X, f y) ≡ f x `o` [^o mset] y ∈ X ∖ {[+ x +]}, f y.
   Proof.
     intros. rewrite -big_opMS_singleton -big_opMS_disj_union.
     by rewrite -gmultiset_disj_union_difference'.
diff --git a/iris/algebra/gmultiset.v b/iris/algebra/gmultiset.v
index e595a307ddaefade23a41194579f84cef5f37042..c7507eefce7dad6ce028739001ba93bddaca57b1 100644
--- a/iris/algebra/gmultiset.v
+++ b/iris/algebra/gmultiset.v
@@ -86,7 +86,7 @@ Section gmultiset.
   Qed.
 
   Lemma big_opMS_singletons X :
-    ([^op mset] x ∈ X, {[ x ]}) = X.
+    ([^op mset] x ∈ X, {[+ x +]}) = X.
   Proof.
     induction X as [|x X IH] using gmultiset_ind.
     - rewrite big_opMS_empty. done.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index b7affdfdcde81325d24fbf8f3fbb9c867c562b9b..824da80c279e7c4f5117cfdf297440e51559c222 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -2053,7 +2053,7 @@ Section gmultiset.
   Proof. apply big_opMS_disj_union. Qed.
 
   Lemma big_sepMS_delete Φ X x :
-    x ∈ X → ([∗ mset] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ mset] y ∈ X ∖ {[ x ]}, Φ y.
+    x ∈ X → ([∗ mset] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ mset] y ∈ X ∖ {[+ x +]}, Φ y.
   Proof. apply big_opMS_delete. Qed.
 
   Lemma big_sepMS_elem_of Φ X x `{!Absorbing (Φ x)} :
@@ -2067,7 +2067,7 @@ Section gmultiset.
     intros. rewrite big_sepMS_delete //. by apply sep_mono_r, wand_intro_l.
   Qed.
 
-  Lemma big_sepMS_singleton Φ x : ([∗ mset] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
+  Lemma big_sepMS_singleton Φ x : ([∗ mset] y ∈ {[+ x +]}, Φ y) ⊣⊢ Φ x.
   Proof. apply big_opMS_singleton. Qed.
 
   Lemma big_sepMS_sep Φ Ψ X :
@@ -2155,7 +2155,7 @@ Section gmultiset.
     Φ x ∗
     (* we reobtain the bigop for a predicate [Ψ] selected by the user *)
     ∀ Ψ,
-      □ (∀ y, ⌜ y ∈ X ∖ {[ x ]} ⌝ → Φ y -∗ Ψ y) -∗
+      □ (∀ y, ⌜ y ∈ X ∖ {[+ x +]} ⌝ → Φ y -∗ Ψ y) -∗
       Ψ x -∗
       [∗ mset] y ∈ X, Ψ y.
   Proof.