diff --git a/opam b/opam
index 96e5496c252c6ddc7fc6f0f5c86c1500eb533a70..3cde3f37e58ecc5ae23204fad6671df5447664ca 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-07-26.8.eb05e835") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-07-28.0.3424ace5") | (= "dev") }
 ]
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index b0b58bd0b71dcc40ae2404d92f0ecb3cb6cab881..f0319c0ca16fc9af0872ed10d5f8dfc2ced1c8b4 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -46,7 +46,7 @@ notions, such as contractiveness and non-expansiveness, after which the
 specifications of the message-passing primitives are defined in terms of the
 protocol connectives. *)
 From iris.algebra Require Import excl_auth.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic Require Export lib.iprop.
 From iris.base_logic Require Import lib.own.
 From iris.program_logic Require Import language.
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 37c8fd0ead7157b66e33e3f31d93fd2048f41b6b..2d5ddb43a323c01564672c8802332d502be69350 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -34,7 +34,7 @@ The defined functions on the type [proto] are:
 - [proto_app], which appends two protocols [p1] and [p2], by substituting
   all terminations [END] in [p1] with [p2]. *)
 From iris.base_logic Require Import base_logic.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From actris.utils Require Import cofe_solver_2.
 Set Default Proof Using "Type".
 
diff --git a/theories/examples/list_rev.v b/theories/examples/list_rev.v
index 0f65fc9189743024fb26c53628258940ce0373bf..2df2afe4be251bc32871725a44fc724e512e69cd 100644
--- a/theories/examples/list_rev.v
+++ b/theories/examples/list_rev.v
@@ -1,5 +1,5 @@
 From actris.channel Require Import proofmode proto channel.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From actris.utils Require Import llist.
 
 Definition list_rev_service : val :=
diff --git a/theories/examples/subprotocols.v b/theories/examples/subprotocols.v
index c6842d47ba3a066d46e4bfaf4f7defa9b8fa0120..7ab8a22687d31a96180607f2ca69222d68582d3c 100644
--- a/theories/examples/subprotocols.v
+++ b/theories/examples/subprotocols.v
@@ -1,5 +1,5 @@
 From actris.channel Require Import proofmode proto channel.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 
 Section subprotocol_basics.
   Context `{heapGS Σ, chanG Σ}.
diff --git a/theories/examples/swap_mapper.v b/theories/examples/swap_mapper.v
index 42446ee7e014a2ea956077083db87a0dc353b406..fb6b29321cff1f23b1abff614c2b5b8bb91f337f 100644
--- a/theories/examples/swap_mapper.v
+++ b/theories/examples/swap_mapper.v
@@ -1,5 +1,5 @@
 From actris.channel Require Import proofmode proto channel.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From actris.utils Require Import llist.
 From iris.heap_lang Require Import notation.
 From actris.examples Require Import sort_fg.
diff --git a/theories/logrel/contexts.v b/theories/logrel/contexts.v
index fe0248a5461528fc5cc44f9ce910115e1bd025d0..1de83166e4cc3636a1f5a1096aed0cbc4ca18138 100644
--- a/theories/logrel/contexts.v
+++ b/theories/logrel/contexts.v
@@ -13,7 +13,7 @@ to the syntactic typing rules that are typically found in substructural type
 systems. *)
 From iris.algebra Require Export list.
 From iris.bi.lib Require Import core.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From actris.logrel Require Export term_types subtyping_rules.
 
 Inductive ctx_item Σ := CtxItem {
diff --git a/theories/logrel/examples/pair.v b/theories/logrel/examples/pair.v
index 6f7a6a562f3448ee488ff0209a98e8e800c1480f..4b8883c79635af166cd5e73e55552707bf7c9b06 100644
--- a/theories/logrel/examples/pair.v
+++ b/theories/logrel/examples/pair.v
@@ -8,7 +8,7 @@ can be assigned the type
 
 by exclusively using the semantic typing rules. *)
 From actris.logrel Require Export term_typing_rules session_typing_rules.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 
 Definition prog : expr := λ: "c", (recv "c", recv "c").
 
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 7ee3bfc814521a135f628028dcff86cbf110072b..ef00bc478b872c4153dcb0584376b201f46bceaa 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -2,7 +2,7 @@
 session types. *)
 From iris.bi.lib Require Import core.
 From iris.base_logic.lib Require Import invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From actris.logrel Require Export subtyping term_types session_types.
 
 Section subtyping_rules.
diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index 52fc272e8bcb5204eb281aff190391ec1057df0d..ce5be825714f843d334543934ec1be3aba8de8da 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -9,7 +9,7 @@ semantically well-typed programs do not get stuck. *)
 From iris.heap_lang Require Import metatheory adequacy.
 From actris.logrel Require Export term_types.
 From actris.logrel Require Export contexts.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 
 (** The semantic typing judgment *)
 Definition ltyped `{!heapGS Σ}
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index 1a7d3af484186ec6f13653eabb9b6c4939703f52..6435034c4797d128f89bca05d7a531f70f80d34c 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -16,7 +16,7 @@ later used in the protocol.
 To model this ghost theory construction, we use the camera
 [auth (option (csum (positive * A) (excl unit)))]. *)
 From iris.base_logic Require Export base_logic lib.iprop lib.own.
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Export proofmode.
 From iris.algebra Require Import excl auth csum gmultiset numbers.
 From iris.algebra Require Export local_updates.