diff --git a/coq-iris.opam b/coq-iris.opam
index 93089a1f9c6991dc50a9d423cc057d6097cb4c5d..bf1fed1f86b0e8f4aee9f7d4129e754d73622340 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 1d91fdb9e2eecc6f2c7c462848d34b39d2bef662..cdbc6298b5765de007a180cbf77109727ac8ba83 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 59808710778d9577b6e8936400b28266f3f2e93a..d6152e97b5860dcd758a74913e266bbd7553c387 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]