From ed2b857ec1ad8b94c0a0fef14237f2e98e0f229b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Jun 2021 22:14:54 +0200
Subject: [PATCH] Bump stdpp.

---
 coq-iris.opam              |  2 +-
 iris/algebra/cmra.v        | 12 ++++++------
 iris/algebra/cmra_big_op.v |  6 +++---
 iris/algebra/gmap.v        |  2 +-
 4 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/coq-iris.opam b/coq-iris.opam
index faed3ff40..07f5e11b1 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -15,7 +15,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-06-16.0.fc5f75e5") | (= "dev") }
+  "coq-stdpp" { (= "dev.2021-06-17.3.3bddee70") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 5dde79ec0..07f46ded4 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -341,13 +341,13 @@ Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.
 
 (** ** Core *)
 Lemma cmra_pcore_l' x cx : pcore x ≡ Some cx → cx ⋅ x ≡ x.
-Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_l. Qed.
+Proof. intros (cx'&?&<-)%Some_equiv_eq. by apply cmra_pcore_l. Qed.
 Lemma cmra_pcore_r x cx : pcore x = Some cx → x ⋅ cx ≡ x.
 Proof. intros. rewrite comm. by apply cmra_pcore_l. Qed.
 Lemma cmra_pcore_r' x cx : pcore x ≡ Some cx → x ⋅ cx ≡ x.
-Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_r. Qed.
+Proof. intros (cx'&?&<-)%Some_equiv_eq. by apply cmra_pcore_r. Qed.
 Lemma cmra_pcore_idemp' x cx : pcore x ≡ Some cx → pcore cx ≡ Some cx.
-Proof. intros (cx'&?&->)%equiv_Some_inv_r'. eauto using cmra_pcore_idemp. Qed.
+Proof. intros (cx'&?&<-)%Some_equiv_eq. eauto using cmra_pcore_idemp. Qed.
 Lemma cmra_pcore_dup x cx : pcore x = Some cx → cx ≡ cx ⋅ cx.
 Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.
 Lemma cmra_pcore_dup' x cx : pcore x ≡ Some cx → cx ≡ cx ⋅ cx.
@@ -412,9 +412,9 @@ Proof. rewrite (comm op); apply cmra_included_l. Qed.
 Lemma cmra_pcore_mono' x y cx :
   x ≼ y → pcore x ≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
 Proof.
-  intros ? (cx'&?&Hcx)%equiv_Some_inv_r'.
+  intros ? (cx'&?&Hcx)%Some_equiv_eq.
   destruct (cmra_pcore_mono x y cx') as (cy&->&?); auto.
-  exists cy; by rewrite Hcx.
+  exists cy; by rewrite -Hcx.
 Qed.
 Lemma cmra_pcore_monoN' n x y cx :
   x ≼{n} y → pcore x ≡{n}≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼{n} cy.
@@ -1126,7 +1126,7 @@ Section prod.
   Lemma prod_pcore_Some' (x cx : A * B) :
     pcore x ≡ Some cx ↔ pcore (x.1) ≡ Some (cx.1) ∧ pcore (x.2) ≡ Some (cx.2).
   Proof.
-    split; [by intros (cx'&[-> ->]%prod_pcore_Some&->)%equiv_Some_inv_r'|].
+    split; [by intros (cx'&[-> ->]%prod_pcore_Some&<-)%Some_equiv_eq|].
     rewrite {3}/pcore /prod_pcore_instance. (* TODO: use setoid rewrite *)
     intros [Hx1 Hx2]; inversion_clear Hx1; simpl; inversion_clear Hx2.
     by constructor.
diff --git a/iris/algebra/cmra_big_op.v b/iris/algebra/cmra_big_op.v
index 71236bbaa..282094e77 100644
--- a/iris/algebra/cmra_big_op.v
+++ b/iris/algebra/cmra_big_op.v
@@ -14,7 +14,7 @@ Lemma big_opM_None {M : cmra} `{Countable K} {A} (f : K → A → option M) m :
   ([^op map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.
 Proof.
   induction m as [|i x m ? IH] using map_ind=> /=; first by rewrite big_opM_eq.
-  rewrite -equiv_None big_opM_insert // equiv_None op_None IH. split.
+  rewrite -None_equiv_eq big_opM_insert // None_equiv_eq op_None IH. split.
   { intros [??] k y. rewrite lookup_insert_Some; naive_solver. }
   intros Hm; split.
   - apply (Hm i). by simplify_map_eq.
@@ -24,13 +24,13 @@ Lemma big_opS_None {M : cmra} `{Countable A} (f : A → option M) X :
   ([^op set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
 Proof.
   induction X as [|x X ? IH] using set_ind_L; [by rewrite big_opS_eq |].
-  rewrite -equiv_None big_opS_insert // equiv_None op_None IH. set_solver.
+  rewrite -None_equiv_eq big_opS_insert // None_equiv_eq op_None IH. set_solver.
 Qed.
 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. multiset_solver. }
-  rewrite -equiv_None big_opMS_disj_union big_opMS_singleton equiv_None op_None IH.
+  rewrite -None_equiv_eq big_opMS_disj_union big_opMS_singleton None_equiv_eq op_None IH.
   multiset_solver.
 Qed.
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index a61482362..55c589952 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -299,7 +299,7 @@ Proof. apply omap_singleton_Some. Qed.
 Lemma singleton_core' (i : K) (x : A) cx :
   pcore x ≡ Some cx → core {[ i := x ]} ≡@{gmap K A} {[ i := cx ]}.
 Proof.
-  intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (singleton_core _ _ cx').
+  intros (cx'&?&<-)%Some_equiv_eq. by rewrite (singleton_core _ _ cx').
 Qed.
 Lemma singleton_core_total `{!CmraTotal A} (i : K) (x : A) :
   core {[ i := x ]} =@{gmap K A} {[ i := core x ]}.
-- 
GitLab