diff --git a/heap_lang/heap_lang_tactics.v b/heap_lang/heap_lang_tactics.v
index f0219d72a89a76d11fdbaa0b6e7e952113c37d22..b94d96a9874822ec7fad7e6ba170587a48b06313 100644
--- a/heap_lang/heap_lang_tactics.v
+++ b/heap_lang/heap_lang_tactics.v
@@ -1,4 +1,4 @@
-Require Export barrier.heap_lang.
+Require Export heap_lang.heap_lang.
 Require Import prelude.fin_maps.
 Import heap_lang.
 
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index a2bd229f72627f67e4aac93a04e1ea0fcb08e783..883d642f611cadf65a992eafa2d8ad5cbb4b415c 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,5 +1,5 @@
 Require Import prelude.gmap iris.lifting.
-Require Export iris.weakestpre barrier.heap_lang_tactics.
+Require Export iris.weakestpre heap_lang.heap_lang_tactics.
 Import uPred.
 Import heap_lang.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
diff --git a/heap_lang/sugar.v b/heap_lang/sugar.v
index 92869fe6990c15df9386c3491ca53619eab5bdce..36b1ab9ddbc423d0151d2f14c7659a9724f54e2e 100644
--- a/heap_lang/sugar.v
+++ b/heap_lang/sugar.v
@@ -1,4 +1,4 @@
-Require Export barrier.heap_lang barrier.lifting.
+Require Export heap_lang.heap_lang heap_lang.lifting.
 Import uPred.
 Import heap_lang.
 
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 667e4f538703a23a2da4cf13373c5dcf83b262d6..c79b53174bb87a9b59784553acf7a7d8126f38a1 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -1,6 +1,6 @@
 (** This file is essentially a bunch of testcases. *)
 Require Import modures.logic.
-Require Import barrier.lifting barrier.sugar.
+Require Import heap_lang.lifting heap_lang.sugar.
 Import heap_lang.
 Import uPred.