From ce8bd0c656a29856cccd667de191017dffd66dca Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Jul 2021 00:20:48 +0200
Subject: [PATCH] Bump std++ (curry/uncurry)

---
 coq-iris.opam                         | 2 +-
 iris/algebra/big_op.v                 | 2 +-
 iris/program_logic/total_weakestpre.v | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/coq-iris.opam b/coq-iris.opam
index 93089a1f9..bf1fed1f8 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.15~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2021-07-19.1.7d502178") | (= "dev") }
+  "coq-stdpp" { (= "dev.2021-07-19.2.e2c65b35") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 1d91fdb9e..cdbc6298b 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -36,7 +36,7 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
    format "[^ o  list]  x  ∈  l ,  P") : stdpp_scope.
 
 Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K → A → M)
-  (m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
+  (m : gmap K A) : M := big_opL o (λ _, uncurry f) (map_to_list m).
 Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
 Definition big_opM := big_opM_aux.(unseal).
 Global Arguments big_opM {M} o {_ K _ _ A} _ _.
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 598087107..d6152e97b 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -45,7 +45,7 @@ Qed.
 Definition twp_pre' `{!irisGS Λ Σ} (s : stuckness) :
   (prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ) →
   prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ :=
-    curry3 ∘ twp_pre s ∘ uncurry3.
+    uncurry3 ∘ twp_pre s ∘ curry3.
 
 Local Instance twp_pre_mono' `{!irisGS Λ Σ} s : BiMonoPred (twp_pre' s).
 Proof.
@@ -54,7 +54,7 @@ Proof.
     iApply twp_pre_mono. iIntros "!>" (E e Φ). iApply ("H" $! (E,e,Φ)).
   - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
       [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
-    rewrite /uncurry3 /twp_pre. do 26 (f_equiv || done). by apply pair_ne.
+    rewrite /curry3 /twp_pre. do 26 (f_equiv || done). by apply pair_ne.
 Qed.
 
 Definition twp_def `{!irisGS Λ Σ} : Twp (iProp Σ) (expr Λ) (val Λ) stuckness
@@ -83,7 +83,7 @@ Lemma twp_ind s Ψ :
   ∀ e E Φ, WP e @ s; E [{ Φ }] -∗ Ψ E e Φ.
 Proof.
   iIntros (HΨ). iIntros "#IH" (e E Φ) "H". rewrite twp_eq.
-  set (Ψ' := curry3 Ψ :
+  set (Ψ' := uncurry3 Ψ :
     prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ).
   assert (NonExpansive Ψ').
   { intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
-- 
GitLab