From 6bf5566ff413327d945b02f8068ca8ad794f0ad2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 13 Mar 2021 11:27:36 +0100
Subject: [PATCH] Replace some uses of `set_solver` by `multiset_solver`.

---
 coq-iris.opam              | 2 +-
 iris/algebra/cmra_big_op.v | 4 ++--
 iris/bi/big_op.v           | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/coq-iris.opam b/coq-iris.opam
index e77d9bb39..7e2db99e9 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.11" & < "8.14~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2021-03-11.0.6d001c9d") | (= "dev") }
+  "coq-stdpp" { (= "dev.2021-03-13.0.7fdaea0f") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/cmra_big_op.v b/iris/algebra/cmra_big_op.v
index 9f105e214..71236bbaa 100644
--- a/iris/algebra/cmra_big_op.v
+++ b/iris/algebra/cmra_big_op.v
@@ -30,7 +30,7 @@ Lemma big_opMS_None {M : cmra} `{Countable A} (f : A → option M) X :
   ([^op mset] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
 Proof.
   induction X as [|x X IH] using gmultiset_ind.
-  { rewrite big_opMS_empty. set_solver. }
+  { rewrite big_opMS_empty. multiset_solver. }
   rewrite -equiv_None big_opMS_disj_union big_opMS_singleton equiv_None op_None IH.
-  set_solver.
+  multiset_solver.
 Qed.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index d0ed67236..b2c883411 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -2103,11 +2103,11 @@ Section gmultiset.
     { by rewrite (affine (â–¡ _)%I) big_sepMS_empty. }
     rewrite intuitionistically_sep_dup big_sepMS_disj_union.
     rewrite big_sepMS_singleton. f_equiv.
-    - rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
+    - rewrite (forall_elim x) pure_True ?True_impl; last multiset_solver.
       by rewrite intuitionistically_elim.
     - rewrite -IH. f_equiv. apply forall_mono=> y.
       apply impl_intro_l, pure_elim_l=> ?.
-      by rewrite pure_True ?True_impl; last set_solver.
+      by rewrite pure_True ?True_impl; last multiset_solver.
   Qed.
 
   Lemma big_sepMS_forall `{BiAffine PROP} Φ X :
-- 
GitLab