diff --git a/_CoqProject b/_CoqProject
index 570535e83fcc12e866c7efcd32e94598586c2e51..46417a25346bf0ed913857e8c0c4fff86c301306 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -73,7 +73,7 @@ program_logic/hoare.v
 program_logic/language.v
 program_logic/ectx_language.v
 program_logic/ectxi_language.v
-program_logic/ectx_weakestpre.v
+program_logic/ectx_lifting.v
 program_logic/ghost_ownership.v
 program_logic/global_functor.v
 program_logic/saved_prop.v
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 157125e2249b2a7679d68a38a70b3e82e56b6e2c..91b78c4f17f66347a1a81265aa040066a0b96135 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,5 +1,5 @@
-From iris.program_logic Require Export ectx_weakestpre.
-From iris.program_logic Require Import ownership. (* for ownP *)
+From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *)
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import weakestpre.
diff --git a/program_logic/ectx_weakestpre.v b/program_logic/ectx_lifting.v
similarity index 100%
rename from program_logic/ectx_weakestpre.v
rename to program_logic/ectx_lifting.v