diff --git a/_CoqProject b/_CoqProject
index 24194d2052b98353a00856f96e9cd1b11f4f041a..6f9545dde7be3d09f967adde7058a95ee5278e79 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -87,7 +87,7 @@ heap_lang/lifting.v
 heap_lang/derived.v
 heap_lang/notation.v
 heap_lang/substitution.v
-heap_lang/lib/heap.v
+heap_lang/heap.v
 heap_lang/lib/spawn.v
 heap_lang/lib/par.v
 heap_lang/lib/assert.v
diff --git a/heap_lang/lib/heap.v b/heap_lang/heap.v
similarity index 100%
rename from heap_lang/lib/heap.v
rename to heap_lang/heap.v
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index d65343ef02f2c6c18de63073272c73ff0a6f8d10..962e6c1e266dfc73d84cf9358e643dd58577f967 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -1,4 +1,4 @@
-From iris.heap_lang Require Export heap spawn.
+From iris.heap_lang Require Export spawn.
 From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index d597b0f986f5f959261d251c14b8bff16e8eed23..52208d3af21aa488e74f32fc9b8782a225fd7156 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -1,5 +1,4 @@
 From iris.program_logic Require Export global_functor.
-From iris.heap_lang Require Export heap.
 From iris.proofmode Require Import invariants ghost_ownership.
 From iris.heap_lang Require Import proofmode notation.
 Import uPred.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 1ac4946399412c15b6200cc82663b43e97eb5eac..5134a793c403618d25c7dac07ec2aea60bde7c24 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import one_shot dec_agree.
 From iris.program_logic Require Import hoare.
-From iris.heap_lang Require Import heap assert proofmode notation.
+From iris.heap_lang Require Import assert proofmode notation.
 From iris.proofmode Require Import invariants ghost_ownership.
 Import uPred.