diff --git a/opam b/opam
index fefdd075f2a74139890c5d1849686e06b8aff5d9..c99b251dc128b90232b54c448b41242ad655a27f 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-06-28.0.c43accd7") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-07-19.3.ce8bd0c6") | (= "dev") }
 ]
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index ec00252151553bf0122a0e089ac35549d29018f2..4c55908cca608ea8b1bd0bd413c449c0be34f79a 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -34,7 +34,7 @@ Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
     (pas : list (bool * iProto Σ)) (q : iProto Σ) :=
   proto_normalize :
     ⊢ iProto_dual_if d p <++>
-        foldr (iProto_app ∘ curry iProto_dual_if) END%proto pas ⊑ q.
+        foldr (iProto_app ∘ uncurry iProto_dual_if) END%proto pas ⊑ q.
 Global Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
 Arguments ProtoNormalize {_} _ _%proto _%proto _%proto.
 
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index a06744b1ddfa4a37740676f2fd00c58ed16c2aeb..62d5dfced188bed808c39c36eea6326dc328675c 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -8,7 +8,7 @@ From iris.algebra Require Import gmultiset.
 (** * Functional version of map reduce (aka the specification) *)
 Definition map_reduce {A B C} `{EqDecision K}
     (map : A → list (K * B)) (red : K → list B → list C) : list A → list C :=
-  mbind (curry red) ∘ group ∘ mbind map.
+  mbind (uncurry red) ∘ group ∘ mbind map.
 Global Instance: Params (@map_reduce) 7 := {}.
 
 (** * Distributed version (aka the implementation) *)
@@ -76,7 +76,7 @@ Section map_reduce.
   Context {A B C} `{EqDecision K} (map : A → list (K * B)) (red : K → list B → list C).
   Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}.
 
-  Global Instance bind_red_perm : Proper ((≡ₚₚ) ==> (≡ₚ)) (mbind (curry red)).
+  Global Instance bind_red_perm : Proper ((≡ₚₚ) ==> (≡ₚ)) (mbind (uncurry red)).
   Proof.
     induction 1 as [|[i1 xs1] [i2 xs2] ixss1 ixss2 [??]|[i1 xs1] [i2 xs2] ixss|];
       simplify_eq/=; try done.
@@ -224,12 +224,12 @@ Section mapper.
       llist IC l zs ∗
       csort ↣ from_option (λ _, sort_fg_tail_protocol IZB RZB iys
         (iys_sorted ++ acc miy)) END%proto miy ∗
-      cred ↣ par_map_protocol IZBs IC (curry red) n (Y : gmultiset (Z * list B)) ∗
+      cred ↣ par_map_protocol IZBs IC (uncurry red) n (Y : gmultiset (Z * list B)) ∗
       from_option (λ '(i,y,w), IB i y w) True miy
     }}}
       par_map_reduce_reduce #n csort cred (accv miy) #l
     {{{ zs', RET #();
-       ⌜ (group iys_sorted ≫= curry red) ++ zs' ≡ₚ (group iys ++ elements Y) ≫= curry red ⌝ ∗
+       ⌜ (group iys_sorted ≫= uncurry red) ++ zs' ≡ₚ (group iys ++ elements Y) ≫= uncurry red ⌝ ∗
        llist IC l (zs' ++ zs)
     }}}.
   Proof.
@@ -275,7 +275,7 @@ Section mapper.
   Lemma par_map_reduce_spec n m vmap vred l xs :
     0 < n → 0 < m →
     map_spec IA IZB map vmap -∗
-    map_spec IZBs IC (curry red) vred -∗
+    map_spec IZBs IC (uncurry red) vred -∗
     {{{ llist IA l xs }}}
       par_map_reduce #n #m vmap vred #l
     {{{ zs, RET #(); ⌜zs ≡ₚ map_reduce map red xs⌝ ∗ llist IC l zs }}}.
@@ -292,7 +292,7 @@ Section mapper.
     wp_smart_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
     iIntros (iys). rewrite gmultiset_elements_empty right_id_L.
     iDestruct 1 as (Hiys) "[Hl Hcsort] /=". wp_select; wp_pures; simpl.
-    wp_smart_apply (start_chan_spec (par_map_protocol IZBs IC (curry red) m ∅));
+    wp_smart_apply (start_chan_spec (par_map_protocol IZBs IC (uncurry red) m ∅));
       iIntros (cred) "// Hcred".
     { wp_pures. wp_smart_apply (par_map_service_spec with "Hred Hcred"); auto. }
     wp_branch as %_|%Hnil; last first.