From 7a260d80710833d00fda6b25c71abdf19d1ec6ad Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Apr 2021 19:02:33 +0200
Subject: [PATCH] Bump std++ (multiset singleton).

---
 coq-iris.opam            | 2 +-
 iris/algebra/big_op.v    | 4 ++--
 iris/algebra/gmultiset.v | 2 +-
 iris/bi/big_op.v         | 6 +++---
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/coq-iris.opam b/coq-iris.opam
index b1b165972..6c1f4a374 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 a56da2ac8..b0f38ffbf 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 e595a307d..c7507eefc 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 b7affdfdc..824da80c2 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.
-- 
GitLab