diff --git a/opam b/opam
index aa2413c08e635076bad81bf4b8ba27ee25ac8cd1..82259addde4540286c91027be36b8ec8753a52ff 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-06-18.0.366d607e") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-07-28.0.3424ace5") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index aeb91c9d682e1c6239b24d9e652bf4c57d9e8b7a..ffbf27b19a7c4582fbdb99e445d8c53f7711fd02 100644
--- a/theories/examples/bit.v
+++ b/theories/examples/bit.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** A simple bit module *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From reloc Require Import reloc.
 Set Default Proof Using "Type".
 
diff --git a/theories/experimental/helping/offers.v b/theories/experimental/helping/offers.v
index 0f86864ba99b3342e713c09c120bfae0a7eea185..f54792c453a60061e137f8fd52b4d6e6aa7ff2fe 100644
--- a/theories/experimental/helping/offers.v
+++ b/theories/experimental/helping/offers.v
@@ -1,7 +1,7 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Offers used to implement the stack with helping
 Based on the case study <https://iris-project.org/pdfs/2017-case-study-concurrent-stacks-with-helping.pdf> *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import excl.
 From reloc Require Export reloc.
 
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index d00cf9bfc15382bc5a0f2e7586d581e5e57b48c4..92c72bb7a63ad8cc171cca278d5792249c68e2ba 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -1,7 +1,7 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Adequacy statements for the refinement proposition *)
 From iris.algebra Require Import auth frac agree.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.heap_lang Require Export adequacy.
 From reloc.logic Require Export spec_ra model.
 
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 3011969923459fe23d81d1d862df1a822c49cae3..31f9d311590b50648e74c0245117e0fd110c91b1 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Compataibility rules *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import list.
 From iris.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Import proofmode.
diff --git a/theories/logic/derived.v b/theories/logic/derived.v
index 6a9376543fcae9ff9a78e4cd5529bca62185ca02..934eef8ae252190801a5120d53a25ceacfec1959 100644
--- a/theories/logic/derived.v
+++ b/theories/logic/derived.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Derived ReLoC rules *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import list.
 From iris.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Import proofmode.
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 95661a170b19039c3d1a5495f1e53e5918c86194..8cfc9bc5f8dd3dfc8f31dc5b6b9ceb4e7cabd724 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import
      reduction.
 From reloc.logic Require Import proofmode.spec_tactics.
 From reloc.logic Require Export model rules derived.
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Export proofmode.
 (* Set Default Proof Using "Type". *)
 
 (** * General-purpose tactics *)
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 7bdb3f9f8eeb01f22e76a49455db07d79bd97ef1..08b628d9b228dfb78d716f29458f77cd4f33568e 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Core ReLoC rules *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import list.
 From iris.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Import proofmode.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index bf0a45ace2882c1aebd202760d0afe6df1455d65..63bb37440faf8f1e9d34a881ef25b44ab8b4cde2 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -3,7 +3,7 @@
 From iris.algebra Require Import auth excl gmap agree list frac.
 From iris.bi Require Export fractional.
 From iris.base_logic Require Export invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.heap_lang Require Import lang primitive_laws.
 Import uPred.
 
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 7cc744d9e2b5794bc0404bc58774b6147f0a9500..a02bc4e21dcc0aa06001945106bb3b5b394c7ac0 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -1,7 +1,7 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Rules for updating the specification program. *)
 From iris.algebra Require Import auth excl frac agree gmap list.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.heap_lang Require Export lang notation tactics.
 From reloc.logic Require Export spec_ra.
 Import uPred.
diff --git a/theories/prelude/bijections.v b/theories/prelude/bijections.v
index a50655c6842766dd5544288450323623db888301..66d630c9ac89278d4b3096d0e1199923dfe095ee 100644
--- a/theories/prelude/bijections.v
+++ b/theories/prelude/bijections.v
@@ -4,7 +4,7 @@ Originally from: "A Logical Relation for Monadic Encapsulation of State: Proving
 by Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal *)
 From iris.algebra Require Import auth gset.
 From iris.base_logic Require Export invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 Import uPred.
 
 Section PBij.
diff --git a/theories/reloc.v b/theories/reloc.v
index fed94d6ead0f73cfecc3d8ae4d0112ce954f3738..bab05af645983890b0d1dbee921b519a83fdb403 100644
--- a/theories/reloc.v
+++ b/theories/reloc.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Export lang notation proofmode.
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Export proofmode.
 From reloc.logic Require Export proofmode.tactics proofmode.spec_tactics model.
 From reloc.logic Require Export rules derived compatibility.
 From reloc.typing Require Export interp tactics soundness.
diff --git a/theories/tests/proofmode_tests.v b/theories/tests/proofmode_tests.v
index d8a8f0a96fca96489cd8da0d382b9c77e9f8c7e7..c1dd406875cccfefbf8667d905f5f36a6be89843 100644
--- a/theories/tests/proofmode_tests.v
+++ b/theories/tests/proofmode_tests.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From reloc.logic.proofmode Require Export spec_tactics tactics.
 From iris.heap_lang Require Import lang notation.
 
diff --git a/theories/tests/tp_tests.v b/theories/tests/tp_tests.v
index 93a20e266586e9840bae30baafbc6c8c1c4e062e..0b7077e433229ccf84963485b40b20229bafe9d4 100644
--- a/theories/tests/tp_tests.v
+++ b/theories/tests/tp_tests.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From reloc.logic Require Export spec_rules proofmode.spec_tactics.
 Set Default Proof Using "Type".
 Import lang.
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index 669627a6b0497c0ea984731c213dd00c3ad771cf..fb1e21f01c5c3dea3720e8488f2a263c6a6c3d38 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -3,7 +3,7 @@
 From Autosubst Require Import Autosubst.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From reloc.prelude Require Import lang_facts.
 From reloc.typing Require Export types interp fundamental.
 
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index c51d82cb53cc0b3e5b82706ea4118b602b426fed..46fcd4df9540b218d82e9389670fdd39c75463a3 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -5,7 +5,7 @@ From iris.heap_lang Require Import proofmode.
 From reloc.logic Require Import model.
 From reloc.logic Require Export rules derived compatibility proofmode.tactics.
 From reloc.typing Require Export interp.
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Export proofmode.
 
 Section fundamental.
   Context `{relocG Σ}.
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 06b3c584ca78d655d7bd12c2d92b02d8a5f55e2e..c1347cd59e09fb7dac10d7e9d7cdbce6c69c4b86 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -2,7 +2,7 @@
 (** Interpretations for System F_mu_ref types *)
 From Autosubst Require Import Autosubst.
 From iris.algebra Require Export list.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From reloc.typing Require Export types.
 From reloc.logic Require Import model.
 From reloc.prelude Require Import properness asubst.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 8be4cdef6afcca20304d4add8f100d27f2fe0c3e..8093802248f6da1007a76df7feafb814a559c784 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Logical relation is sound w.r.t. the contextual refinement. *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From reloc.logic Require Export adequacy.
 From reloc.typing Require Export contextual_refinement.