From e2ea7f16049b9f85c7efd67626c27d739974d0ee Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 26 Jul 2021 19:59:41 +0200
Subject: [PATCH] adjust imports

---
 iris/base_logic/bupd_alt.v                  | 2 +-
 iris/base_logic/lib/boxes.v                 | 2 +-
 iris/base_logic/lib/cancelable_invariants.v | 2 +-
 iris/base_logic/lib/fancy_updates.v         | 2 +-
 iris/base_logic/lib/fancy_updates_from_vs.v | 2 +-
 iris/base_logic/lib/gen_heap.v              | 2 +-
 iris/base_logic/lib/gen_inv_heap.v          | 2 +-
 iris/base_logic/lib/ghost_map.v             | 2 +-
 iris/base_logic/lib/ghost_var.v             | 2 +-
 iris/base_logic/lib/gset_bij.v              | 2 +-
 iris/base_logic/lib/invariants.v            | 2 +-
 iris/base_logic/lib/mono_nat.v              | 2 +-
 iris/base_logic/lib/na_invariants.v         | 2 +-
 iris/base_logic/lib/proph_map.v             | 2 +-
 iris/base_logic/lib/saved_prop.v            | 2 +-
 iris/base_logic/lib/wsat.v                  | 2 +-
 iris/bi/lib/atomic.v                        | 2 +-
 iris/bi/lib/core.v                          | 2 +-
 iris/bi/lib/counterexamples.v               | 2 +-
 iris/bi/lib/fixpoint.v                      | 2 +-
 iris/bi/lib/laterable.v                     | 2 +-
 iris/bi/lib/relations.v                     | 2 +-
 iris/program_logic/adequacy.v               | 2 +-
 iris/program_logic/atomic.v                 | 2 +-
 iris/program_logic/ectx_lifting.v           | 2 +-
 iris/program_logic/lifting.v                | 2 +-
 iris/program_logic/ownp.v                   | 2 +-
 iris/program_logic/total_adequacy.v         | 2 +-
 iris/program_logic/total_ectx_lifting.v     | 2 +-
 iris/program_logic/total_lifting.v          | 2 +-
 iris/program_logic/total_weakestpre.v       | 2 +-
 iris/program_logic/weakestpre.v             | 2 +-
 iris/proofmode/monpred.v                    | 2 +-
 iris_heap_lang/adequacy.v                   | 2 +-
 iris_heap_lang/derived_laws.v               | 2 +-
 iris_heap_lang/lib/arith.v                  | 2 +-
 iris_heap_lang/lib/array.v                  | 2 +-
 iris_heap_lang/lib/assert.v                 | 2 +-
 iris_heap_lang/lib/atomic_heap.v            | 2 +-
 iris_heap_lang/lib/counter.v                | 2 +-
 iris_heap_lang/lib/diverge.v                | 2 +-
 iris_heap_lang/lib/increment.v              | 2 +-
 iris_heap_lang/lib/spawn.v                  | 2 +-
 iris_heap_lang/lib/spin_lock.v              | 2 +-
 iris_heap_lang/lib/ticket_lock.v            | 2 +-
 iris_heap_lang/primitive_laws.v             | 2 +-
 iris_heap_lang/total_adequacy.v             | 2 +-
 47 files changed, 47 insertions(+), 47 deletions(-)

diff --git a/iris/base_logic/bupd_alt.v b/iris/base_logic/bupd_alt.v
index e97df5dd1..568b27cb9 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 8a00bc3a2..f86854d37 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 88b0cda57..0f6c3804c 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 3feb1b40c..f2f48b43a 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 a3d331e04..1be809580 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 a0a086c8d..467b9f90c 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 359b0009e..e3b57bbcf 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 2b4b6f46d..d8a8d713f 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 6b23455dc..d3a4b17a6 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 45f6a84e4..01eff6928 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 620c5994e..a44748681 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 ba3d1cef3..e3794680c 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 1f44bab6e..f94042796 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 44d78abe6..98693dd34 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 0c7559332..51c2892da 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 b2c2f27ce..1b3b210d7 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 13bfe0465..44e01693b 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 195de23af..94d004fbd 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 405653f33..534a2e559 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 45ca41fcb..141e1c9e2 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 797b54a15..fdd78566f 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 a00a710d9..658e64a9b 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 2b06be13b..e26604eaa 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 8feb932af..1ca7a0f1e 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 1dd14d2b2..74532a115 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 edc7b8f81..2e7845f67 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 60d7e4507..ef838305f 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 3070bdc5d..3284ced1b 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 473b61acb..76fb2ff1c 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 aac06d858..c2a1214ac 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 d33ca14eb..f390e3009 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 22b5565f0..db92ff28d 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 bc90575ed..860df49d9 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 3ce089fac..42814e06e 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 f1627aa09..f9553c03e 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 17f037256..26f5cd785 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 4508f0fef..ec22b73ed 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 a63b674ec..58dbd164a 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 af057db21..cb216f66c 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 334e091df..430fec3d4 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 cc6fb28eb..ae9767278 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 3f166ca57..639fbf761 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 f2f9aa9c9..75b7aac74 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 1a3ed783f..fe600a2a5 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 a6b343d71..31ddba659 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 d4e9f2484..e70d0ff1d 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 327a287c1..a0389c87f 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.
-- 
GitLab