diff --git a/iris/base_logic/bupd_alt.v b/iris/base_logic/bupd_alt.v
index e97df5dd1b09775cc0083ae0a92ca8accad21f6a..568b27cb9f5176e71f33e9aa677087e68afb2c4e 100644
--- a/iris/base_logic/bupd_alt.v
+++ b/iris/base_logic/bupd_alt.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic Require Export base_logic.
 From iris.prelude Require Import options.
 
diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index 8a00bc3a20228014469ac11f0e0877eea11ff9f7..f86854d379282b82a437ca51e60a253a7424b606 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import lib.excl_auth gmap agree.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
 Import uPred.
diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index 88b0cda572e65a1bf4694c7d42b4ae1df7586638..0f6c3804c99255fc1417477f55248797ba92907b 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export frac.
 From iris.bi.lib Require Import fractional.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
 Import uPred.
diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index 3feb1b40cdb439053541a794f7e7bf4e3b4364a0..f2f48b43a8c0a5d6faf0a3ef0123aae89886396c 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -1,6 +1,6 @@
 From stdpp Require Export coPset.
 From iris.algebra Require Import gmap auth agree gset coPset.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import wsat.
 From iris.prelude Require Import options.
diff --git a/iris/base_logic/lib/fancy_updates_from_vs.v b/iris/base_logic/lib/fancy_updates_from_vs.v
index a3d331e041f048674db04cac979bded9958ef859..1be809580332bb8ba2e5532eaa2b4d97d49a344f 100644
--- a/iris/base_logic/lib/fancy_updates_from_vs.v
+++ b/iris/base_logic/lib/fancy_updates_from_vs.v
@@ -2,7 +2,7 @@
 view shift, and that the laws of the fancy update can be derived from the
 laws of the view shift. *)
 From stdpp Require Export coPset.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic Require Export base_logic.
 From iris.prelude Require Import options.
 
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index a0a086c8deba6f71aa37f674d6450773ea30f86f..467b9f90cd1c695b3d2ab0e5c16ef6f9e404d63e 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -2,7 +2,7 @@ From stdpp Require Export namespaces.
 From iris.algebra Require Import reservation_map agree frac.
 From iris.algebra Require Export dfrac.
 From iris.bi.lib Require Import fractional.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import ghost_map.
 From iris.prelude Require Import options.
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index 359b0009e9312544db1a2ae3bf996fdc6868bf6e..e3b57bbcf5238a3022ea7a24523175d8ce36abee 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import auth excl gmap.
 From iris.base_logic.lib Require Import own invariants gen_heap.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.prelude Require Import options.
 
 (** An "invariant" location is a location that has some invariant about its
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index 2b4b6f46d26703a548dc0775dd563e955857a48c..d8a8d713f30a81c37ae9a94b0a9b21f5f3c52dff 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -2,7 +2,7 @@
 ownership of the entire heap, and a "points-to-like" proposition for (mutable,
 fractional, or persistent read-only) ownership of individual elements. *)
 From iris.bi.lib Require Import fractional.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import gmap_view.
 From iris.algebra Require Export dfrac.
 From iris.base_logic.lib Require Export own.
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 6b23455dce48b04d8f5ce1ca67e271b12b76f5ba..d3a4b17a693c05adc9630b3163d9b6ace3075028 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -2,7 +2,7 @@
 Can be mutated when fully owned. *)
 From iris.algebra Require Import frac_agree.
 From iris.bi.lib Require Import fractional.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export own.
 From iris.prelude Require Import options.
 
diff --git a/iris/base_logic/lib/gset_bij.v b/iris/base_logic/lib/gset_bij.v
index 45f6a84e4a63518055fc007f21a9779e20e3fb1b..01eff6928c3000667b98bf8930661b868bbd006a 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -23,7 +23,7 @@ This library is a logical, ownership-based wrapper around [gset_bij]. *)
 From iris.algebra.lib Require Import gset_bij.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import own.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.prelude Require Import options.
 
 (* The uCMRA we need. *)
diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index 620c5994e805de3324683e76cc1f4c670099b087..a447486815982a59364f9b5bb0c334e62d0b8ca8 100644
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -1,6 +1,6 @@
 From stdpp Require Export namespaces.
 From iris.algebra Require Import gmap.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export fancy_updates.
 From iris.base_logic.lib Require Import wsat.
 From iris.prelude Require Import options.
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index ba3d1cef3a6bb99b383c442fe58a76ea2bca85ca..e3794680c39796c912d9bc7faea69be45ad2d54d 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -7,7 +7,7 @@ The key rules are [mono_nat_lb_own_valid], which asserts that an auth at [n] and
 a lower-bound at [m] imply that [m ≤ n], and [mono_nat_update], which allows to
 increase the auth element. At any time the auth nat can be "snapshotted" with
 [mono_nat_get_lb] to produce a persistent lower-bound proposition. *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra.lib Require Import mono_nat.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Export own.
diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index 1f44bab6eb109064912b75930dc4be8975c36b5e..f940427961e74c0d345cafd69b20bb3bc7ae9215 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import gset coPset.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
 Import uPred.
diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index 44d78abe6d76da090683c7082f71f996e213f36e..98693dd34c62fe96599fb5f02f3aa857ada4cdd7 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import ghost_map.
 From iris.prelude Require Import options.
diff --git a/iris/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
index 0c7559332e402282c98c2d27cdda36e7a480bd2d..51c2892da46839fc5308a3ad1cffdfe05dafb44a 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap.
 From iris.algebra Require Import agree.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic Require Export own.
 From iris.prelude Require Import options.
 Import uPred.
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index b2c2f27cef10c8965f9266e9891a8f61f8f19a27..1b3b210d772a941fc1c84877938aae411aa01f55 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -1,6 +1,6 @@
 From stdpp Require Export coPset.
 From iris.algebra Require Import gmap_view gset coPset.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export own.
 From iris.prelude Require Import options.
 
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 13bfe0465e9261b32ae69613f4192af7482a2414..44e01693b37efaeaba7eb0f2d6de5772d97d25ac 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -1,7 +1,7 @@
 From stdpp Require Import coPset namespaces.
 From iris.bi Require Export bi updates laterable.
 From iris.bi.lib Require Import fixpoint.
-From iris.proofmode Require Import coq_tactics tactics reduction.
+From iris.proofmode Require Import coq_tactics proofmode reduction.
 From iris.prelude Require Import options.
 
 (** Conveniently split a conjunction on both assumption and conclusion. *)
diff --git a/iris/bi/lib/core.v b/iris/bi/lib/core.v
index 195de23afa45a9920e967ea785b27da3c0183878..94d004fbdaa40e3aa098e88a50ba41649a75913d 100644
--- a/iris/bi/lib/core.v
+++ b/iris/bi/lib/core.v
@@ -1,5 +1,5 @@
 From iris.bi Require Export bi plainly.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.prelude Require Import options.
 Import bi.
 
diff --git a/iris/bi/lib/counterexamples.v b/iris/bi/lib/counterexamples.v
index 405653f33cc27777b2ca9902ddda5847c29da090..534a2e559275610eb36c58cc8f659d155b6d9e15 100644
--- a/iris/bi/lib/counterexamples.v
+++ b/iris/bi/lib/counterexamples.v
@@ -1,5 +1,5 @@
 From iris.bi Require Export bi.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.prelude Require Import options.
 
 (* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index 45ca41fcb7d4c2562b58bf417e6f9a627bbb54ff..141e1c9e2e945ce7a388a3e079cedff97f54f1f4 100644
--- a/iris/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -1,5 +1,5 @@
 From iris.bi Require Export bi.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.prelude Require Import options.
 Import bi.
 
diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v
index 797b54a15580e0cbfa3cf3272a1794988d32924f..fdd78566f44d3954a1e5fd4c106a7c5dfc02856e 100644
--- a/iris/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -1,5 +1,5 @@
 From iris.bi Require Export bi.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.prelude Require Import options.
 
 (** The class of laterable assertions *)
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index a00a710d99c1511c002fa52fe3e6e4f0f4064b7e..658e64a9bcbff0c6e893a9914a5babc9464a4d1b 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -1,7 +1,7 @@
 (** This file provides a construction to lift a PROP-level binary relation to
 its reflexive transitive closure. *)
 From iris.bi.lib Require Export fixpoint.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.prelude Require Import options.
 
 (* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 2b06be13b600bc31191179c818239a1cefe43c87..e26604eaa97e23ddf8365d2b3d00ad1be18a3a0c 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import gmap auth agree gset coPset.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Import wsat.
 From iris.program_logic Require Export weakestpre.
 From iris.prelude Require Import options.
diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index 8feb932af91cb7f2e68973dcbc18f811215a74f4..1ca7a0f1ea390c00f8f2396a7b36587a7d5c770b 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -1,7 +1,7 @@
 From stdpp Require Import namespaces.
 From iris.bi Require Import telescopes.
 From iris.bi.lib Require Export atomic.
-From iris.proofmode Require Import tactics classes.
+From iris.proofmode Require Import proofmode classes.
 From iris.program_logic Require Export weakestpre.
 From iris.base_logic Require Import invariants.
 From iris.prelude Require Import options.
diff --git a/iris/program_logic/ectx_lifting.v b/iris/program_logic/ectx_lifting.v
index 1dd14d2b21d473d2b55a07c450fc4b5cf7939950..74532a115b07a52305b5eff6e88c8eadbb6bf1ec 100644
--- a/iris/program_logic/ectx_lifting.v
+++ b/iris/program_logic/ectx_lifting.v
@@ -1,5 +1,5 @@
 (** Some derived lemmas for ectx-based languages *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.prelude Require Import options.
 
diff --git a/iris/program_logic/lifting.v b/iris/program_logic/lifting.v
index edc7b8f81796023de05ef97b98b70181cafacef3..2e7845f6796cfc22d400bef358a4025d2f20d654 100644
--- a/iris/program_logic/lifting.v
+++ b/iris/program_logic/lifting.v
@@ -1,7 +1,7 @@
 (** The "lifting lemmas" in this file serve to lift the rules of the operational
 semantics to the program logic. *)
 
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export weakestpre.
 From iris.prelude Require Import options.
 
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 60d7e4507d7fe474042b72e3feac3fd0375d2476..ef838305f6eea1226366bb1e561505be9da76da7 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import lib.excl_auth.
-From iris.proofmode Require Import tactics classes.
+From iris.proofmode Require Import proofmode classes.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 3070bdc5d009dafecd01c0c7c96f0e581475d815..3284ced1b2eeee22924438eb954fe0ffae436bc0 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import gmap auth agree gset coPset list.
 From iris.bi Require Import big_op fixpoint.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export total_weakestpre adequacy.
 From iris.prelude Require Import options.
 Import uPred.
diff --git a/iris/program_logic/total_ectx_lifting.v b/iris/program_logic/total_ectx_lifting.v
index 473b61acb7fda9a255b61ca501977ed076c61cc1..76fb2ff1c75f8f5145d76bb7c01b16a2a631501f 100644
--- a/iris/program_logic/total_ectx_lifting.v
+++ b/iris/program_logic/total_ectx_lifting.v
@@ -1,5 +1,5 @@
 (** Some derived lemmas for ectx-based languages *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export ectx_language total_weakestpre total_lifting.
 From iris.prelude Require Import options.
 
diff --git a/iris/program_logic/total_lifting.v b/iris/program_logic/total_lifting.v
index aac06d858ba1e4975343862e58535c177f755893..c2a1214ac5b79cfd0c717e19081778cb6870db53 100644
--- a/iris/program_logic/total_lifting.v
+++ b/iris/program_logic/total_lifting.v
@@ -1,5 +1,5 @@
 From iris.bi Require Export big_op.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export total_weakestpre.
 From iris.prelude Require Import options.
 
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index d33ca14ebff44e96878ee9d996b02897dfd87a2a..f390e3009eef7f7595cfa076bab34119b5fb5a11 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -1,5 +1,5 @@
 From iris.bi Require Import fixpoint big_op.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export weakestpre.
 From iris.prelude Require Import options.
 Import uPred.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 22b5565f05e5d1b9de07ecb037563be7ff251386..db92ff28df23469153892dce60ee00074454089b 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import base tactics classes.
+From iris.proofmode Require Import base proofmode classes.
 From iris.base_logic.lib Require Export fancy_updates.
 From iris.program_logic Require Export language.
 (* FIXME: If we import iris.bi.weakestpre earlier texan triples do not
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index bc90575eda6adfe2ba37f35821893d96164c7649..860df49d9bca5e39f28eda07808aab78e8458172 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -1,6 +1,6 @@
 From iris.bi Require Export monpred.
 From iris.bi Require Import plainly.
-From iris.proofmode Require Import tactics modality_instances.
+From iris.proofmode Require Import proofmode modality_instances.
 From iris.prelude Require Import options.
 
 Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
diff --git a/iris_heap_lang/adequacy.v b/iris_heap_lang/adequacy.v
index 3ce089faca66180d9fc8d2e19866c25f80785f74..42814e06e6ed009146c21a9cd4faf7187639c751 100644
--- a/iris_heap_lang/adequacy.v
+++ b/iris_heap_lang/adequacy.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import auth.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Import proofmode notation.
 From iris.prelude Require Import options.
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index f1627aa097c34f03a16de836f2b744bb6055d692..f9553c03e5afc3f31fbf65eb55dc20a10946be2f 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -6,7 +6,7 @@ For utility functions on arrays (e.g., freeing/copying an array), see
 
 From stdpp Require Import fin_maps.
 From iris.bi Require Import lib.fractional.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.heap_lang Require Export primitive_laws.
 From iris.heap_lang Require Import tactics notation.
 From iris.prelude Require Import options.
diff --git a/iris_heap_lang/lib/arith.v b/iris_heap_lang/lib/arith.v
index 17f037256aa5eb72d41ecbd8b704821aa7915ea3..26f5cd785ca0b4da66b1367bd576de6f20c75bef 100644
--- a/iris_heap_lang/lib/arith.v
+++ b/iris_heap_lang/lib/arith.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/iris_heap_lang/lib/array.v b/iris_heap_lang/lib/array.v
index 4508f0fefa0c9dd8d817ae45a82081eb44c1a0eb..ec22b73ed96fc7e8a77702ea0050e3349df8e282 100644
--- a/iris_heap_lang/lib/array.v
+++ b/iris_heap_lang/lib/array.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export derived_laws.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/iris_heap_lang/lib/assert.v b/iris_heap_lang/lib/assert.v
index a63b674ec8284c46f398a953f01aeb3c32c96993..58dbd164a3fb64cf964d8ef3bc19a3d47f4f8b9a 100644
--- a/iris_heap_lang/lib/assert.v
+++ b/iris_heap_lang/lib/assert.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index af057db21b019cb21539a38ee516eae530f645c0..cb216f66cc83d6100e3b34efe18beddd7d8e3533 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -1,5 +1,5 @@
 From iris.bi.lib Require Import fractional.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export atomic.
 From iris.heap_lang Require Export derived_laws.
 From iris.heap_lang Require Import notation proofmode.
diff --git a/iris_heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
index 334e091df3270fcc4f83d515fb27d2a4c5615ce2..430fec3d41676dd352d221eb3af67e87db3bef5e 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import lib.frac_auth numbers auth.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
diff --git a/iris_heap_lang/lib/diverge.v b/iris_heap_lang/lib/diverge.v
index cc6fb28ebb726c43b81cda573bf1a47657238da8..ae976727843aa63b4866208ad1d4c704aed153de 100644
--- a/iris_heap_lang/lib/diverge.v
+++ b/iris_heap_lang/lib/diverge.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index 3f166ca57fed2443af255856593069632c0e652b..639fbf761e8c898b122a3603dd4d1cb96d8a38c4 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -1,5 +1,5 @@
 From iris.bi.lib Require Import fractional.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export atomic.
 From iris.heap_lang Require Import proofmode notation atomic_heap par.
diff --git a/iris_heap_lang/lib/spawn.v b/iris_heap_lang/lib/spawn.v
index f2f9aa9c987cee0397a0745cd75dac8077284dec..75b7aac74284bea68c5b613c03b1ec055c688877 100644
--- a/iris_heap_lang/lib/spawn.v
+++ b/iris_heap_lang/lib/spawn.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import excl.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 1a3ed783ff39eaacf63becad029bbfa9bfbfc0f1..fe600a2a51d1b5b8e552db6503e13154fd383692 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import excl.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index a6b343d7145d2f5370483d415f4238a29b2d1f6a..31ddba65967f107329fd884d98736686e9908ff6 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import excl auth gset.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index d4e9f24847b5dde0f7edf86e675e4fd7898c6195..e70d0ff1d6ef35244236c21a63f27026f506768c 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -1,7 +1,7 @@
 (** This file proves the basic laws of the HeapLang program logic by applying
 the Iris lifting lemmas. *)
 
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap.
 From iris.program_logic Require Export weakestpre total_weakestpre.
diff --git a/iris_heap_lang/total_adequacy.v b/iris_heap_lang/total_adequacy.v
index 327a287c1c9329e06c6266264fb60f79f281bd17..a0389c87f65d1b4b0dc8a9a6605f81f89f981617 100644
--- a/iris_heap_lang/total_adequacy.v
+++ b/iris_heap_lang/total_adequacy.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export total_adequacy.
 From iris.heap_lang Require Export adequacy.
 From iris.heap_lang Require Import proofmode notation.