diff --git a/heap_lang/lib/assert.v b/heap_lang/lib/assert.v
index 4e62f488b3535afc4aafb4d28d83f4cc739f0717..bae4e2c03d608dda2f547c1ed3e7e6f9e34a37db 100644
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
@@ -1,3 +1,5 @@
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 5b43b5fdd4959633913a079454b021108d208977..55c8a2fc499ddd90c8199bce339cf00e6765191e 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -1,8 +1,10 @@
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang.lib.barrier Require Export barrier.
 From iris.prelude Require Import functions.
 From iris.algebra Require Import upred_big_op.
 From iris.program_logic Require Import saved_prop sts.
 From iris.heap_lang Require Import proofmode.
-From iris.heap_lang.lib.barrier Require Export barrier.
 From iris.heap_lang.lib.barrier Require Import protocol.
 
 (** The CMRAs we need. *)
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index e1677077e65c8c9b33784b1c6cb5c9e6e3baa11d..9678f3f5d451f05dd064aa2d280f2b03aac15ee0 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -1,3 +1,4 @@
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import invariants tactics.
 From iris.program_logic Require Import auth.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 080bb3d6c75fade5469301709b1487bcad661a71..6f3b9b5bdcaa0dfda960baaf6b858372ce6abbb6 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -1,3 +1,4 @@
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import invariants tactics.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index af61860e222ac7d1a4acfd2f4c580a61774e4ca0..dfdd1bceff936d28247f54fb2a7a042282149721 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -1,3 +1,4 @@
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import invariants tactics.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 19094846864650174969f1cb40bbea13ff5ae571..35f0f53db6c8aba2380bff7feb21dedc0ab65195 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -1,5 +1,7 @@
-From iris.program_logic Require Export global_functor auth.
-From iris.proofmode Require Import invariants ghost_ownership.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.program_logic Require Import auth.
+From iris.proofmode Require Import invariants.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import gset.
 Import uPred.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index cd77b305200cc8e45c22c48f128742964145ec90..996e74578b4ed46460c14dac9fc0869ddfa7e4ec 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -1,7 +1,7 @@
-From iris.algebra Require Export auth upred_tactics.
+From iris.program_logic Require Export pviewshifts.
+From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
-From iris.program_logic Require Export invariants ghost_ownership.
-From iris.proofmode Require Import invariants ghost_ownership.
+From iris.proofmode Require Import invariants.
 Import uPred.
 
 (* The CMRA we need. *)
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 59308593d091395e32a5e8da2214d7d66987fa5e..97a46c231fdb095347c590bfbef6efd07a22353e 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Import gmap agree upred_big_op.
-From iris.program_logic Require Import auth saved_prop.
+From iris.program_logic Require Export pviewshifts.
+From iris.algebra Require Import auth gmap agree upred_big_op.
 From iris.proofmode Require Import tactics invariants.
 Import uPred.
 
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 671ee6aa949338e35dda7ca5bccdfbb90fd36ff6..e331e34c978d75f172783a60c0aa96ac2278dc53 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Export sts upred_tactics.
-From iris.program_logic Require Export invariants.
+From iris.program_logic Require Export pviewshifts.
+From iris.algebra Require Export sts.
 From iris.proofmode Require Import invariants.
 Import uPred.
 
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 111c5aea534db3ab49b54187db83ffc50cc8a8b5..42fe6db300183f04f9b2716338358c7e5b531785 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -1,8 +1,9 @@
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
 From iris.heap_lang.lib.barrier Require Import proof.
 From iris.heap_lang Require Import par.
 From iris.program_logic Require Import auth sts saved_prop hoare ownership.
 From iris.heap_lang Require Import proofmode.
-Import uPred.
 
 Definition worker (n : Z) : val :=
   λ: "b" "y", wait "b" ;; !"y" #n.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 932aac1d352e38b0c45df8482fde182d70172d4f..c3665bfbc867e6501b7df7f300e601374091104f 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,5 +1,7 @@
 (** This file is essentially a bunch of testcases. *)
-From iris.program_logic Require Import ownership hoare auth.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.program_logic Require Import ownership hoare.
 From iris.heap_lang Require Import proofmode notation.
 
 Section LangTests.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index e5d2f1f4e5381ac04797db34d7444a546f1de6bb..2ddf7d55c19c83fa65914a52b3c50c126cd4ac45 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -1,5 +1,6 @@
+From iris.program_logic Require Export weakestpre hoare.
+From iris.heap_lang Require Export lang.
 From iris.algebra Require Import excl agree csum.
-From iris.program_logic Require Import hoare.
 From iris.heap_lang.lib.barrier Require Import proof specification.
 From iris.heap_lang Require Import notation par proofmode.
 From iris.proofmode Require Import invariants.
@@ -54,7 +55,7 @@ Lemma Q_res_join γ : barrier_res γ Ψ1 ★ barrier_res γ Ψ2 ⊢ ▷ barrier_
 Proof.
   iIntros "[Hγ Hγ']";
   iDestruct "Hγ" as (x) "[#Hγ Hx]"; iDestruct "Hγ'" as (x') "[#Hγ' Hx']".
-  iAssert (▷ (x ≡ x'))%I as "Hxx" .
+  iAssert (▷ (x ≡ x'))%I as "Hxx".
   { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
     rewrite own_valid csum_validI /= agree_validI agree_equivI uPred.later_equivI /=.
     rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index dafe2070bee7fca57a914073eb8719f472b7eee1..4ab90f4c54e09c4e985c21c8c9415ac464f98a25 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -1,6 +1,7 @@
 (** Correctness of in-place list reversal *)
+From iris.program_logic Require Export weakestpre hoare.
+From iris.heap_lang Require Export lang.
 From iris.proofmode Require Export tactics.
-From iris.program_logic Require Export hoare.
 From iris.heap_lang Require Import proofmode notation.
 
 Section list_reverse.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index e644474e60c39b8526ed5e3dabc25feec7be8d9e..e09c317b6df34228b78b4aacce2280e6e9b6e3f2 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -1,7 +1,8 @@
+From iris.program_logic Require Export weakestpre hoare.
+From iris.heap_lang Require Export lang.
 From iris.algebra Require Import excl dec_agree csum.
-From iris.program_logic Require Import hoare.
 From iris.heap_lang Require Import assert proofmode notation.
-From iris.proofmode Require Import invariants ghost_ownership.
+From iris.proofmode Require Import invariants.
 
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index d188e64b6549a5b16602d635edcb59e9c11e7c0d..18a8a4d892215f952aecd6d9b09ae47c2216c8dd 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -1,3 +1,5 @@
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.