diff --git a/_CoqProject b/_CoqProject
index b4ace7a2868434ad97fc79e1203dc36c09c365e3..e7841b5a09a85c12aca08a8f39aef49b342e92f5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -83,6 +83,7 @@ theories/base_logic/lib/na_invariants.v
 theories/base_logic/lib/cancelable_invariants.v
 theories/base_logic/lib/counter_examples.v
 theories/base_logic/lib/fractional.v
+theories/base_logic/lib/gen_heap.v
 theories/program_logic/adequacy.v
 theories/program_logic/lifting.v
 theories/program_logic/weakestpre.v
@@ -91,7 +92,6 @@ theories/program_logic/language.v
 theories/program_logic/ectx_language.v
 theories/program_logic/ectxi_language.v
 theories/program_logic/ectx_lifting.v
-theories/program_logic/gen_heap.v
 theories/program_logic/ownp.v
 theories/heap_lang/lang.v
 theories/heap_lang/tactics.v
diff --git a/theories/program_logic/gen_heap.v b/theories/base_logic/lib/gen_heap.v
similarity index 100%
rename from theories/program_logic/gen_heap.v
rename to theories/base_logic/lib/gen_heap.v
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 861e50cefadbf4cc99cb7c6b4b98108399cfbe28..9d3dfeb8f934ef12463cd28c8804369ab5e342cb 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -1,4 +1,5 @@
-From iris.program_logic Require Export weakestpre gen_heap.
+From iris.base_logic Require Export gen_heap.
+From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.