diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index e3769b7017c9ed245801eb3b9fdb4e57f52c1bc0..c5edacc8eeeea494959653d3494778ce3abb528d 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -1,7 +1,6 @@
 From stdpp Require Import fin_maps.
 From iris.bi Require Import lib.fractional.
 From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export total_weakestpre weakestpre.
 From iris.heap_lang Require Export lifting.
 From iris.heap_lang Require Import tactics notation.
 Set Default Proof Using "Type".
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 4660d56046257f538f37df0dac256c7b5c8e8905..9f403fd1a81c6296a7484b44cef8045725870fe6 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap.
 From iris.base_logic Require Export gen_heap.
 From iris.base_logic.lib Require Export proph_map.
-From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics notation.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 2851575e316f241e211dd63dde579bfc62b41d47..98ea0e6758ebc15bcc7577466f5034ad664f91ba 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -1,8 +1,7 @@
 From iris.proofmode Require Import coq_tactics reduction.
 From iris.proofmode Require Export tactics.
-From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.program_logic Require Import atomic.
-From iris.heap_lang Require Export tactics lifting array.
+From iris.heap_lang Require Export tactics array.
 From iris.heap_lang Require Import notation.
 Set Default Proof Using "Type".
 Import uPred.