diff --git a/_CoqProject b/_CoqProject
index 1332a4ef08350e0688ab1216cf1e5401303ce84b..c075b17c69a39fe0a58c2d617d67e2d4816716c3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -95,8 +95,8 @@ theories/program_logic/gen_heap.v
 theories/program_logic/ownp.v
 theories/heap_lang/lang.v
 theories/heap_lang/tactics.v
+theories/heap_lang/lifting.v
 theories/heap_lang/wp_tactics.v
-theories/heap_lang/op_rules.v
 theories/heap_lang/notation.v
 theories/heap_lang/lib/spawn.v
 theories/heap_lang/lib/par.v
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index de6640d5ea55e1f7aaa613292d1b4fb3121f3cf4..295fe6a8ae4a721aa94c92f818932ebd0c09eb3d 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre adequacy gen_heap.
-From iris.heap_lang Require Export op_rules.
+From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
diff --git a/theories/heap_lang/op_rules.v b/theories/heap_lang/lifting.v
similarity index 99%
rename from theories/heap_lang/op_rules.v
rename to theories/heap_lang/lifting.v
index 55b665f43a982f3e71ccefe7c7520f6f1a4f9f4d..807ae26b565fcd4ba3c95c44b626ae1b74a61f45 100644
--- a/theories/heap_lang/op_rules.v
+++ b/theories/heap_lang/lifting.v
@@ -52,7 +52,7 @@ Local Hint Constructors head_step.
 Local Hint Resolve alloc_fresh.
 Local Hint Resolve to_of_val.
 
-Section rules.
+Section lifting.
 Context `{heapG Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
@@ -276,4 +276,4 @@ Proof.
   intros. rewrite -wp_bin_op //; [].
   destruct (bool_decide_reflect (v1 = v2)); by eauto.
 Qed.
-End rules.
+End lifting.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index acee4c4ec0d7328e437b05ef4175fed1feaf30fe..e0465a37acc1cf7b5fafcceda721fb78e4ae13a9 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
-From iris.heap_lang Require Export wp_tactics op_rules.
+From iris.heap_lang Require Export wp_tactics lifting.
 Import uPred.
 
 Ltac wp_strip_later ::= iNext.
diff --git a/theories/heap_lang/wp_tactics.v b/theories/heap_lang/wp_tactics.v
index d7cf79c912f5341e749a2c31ffc2efe48fd33b7f..16e01deefeab7da0d66842ead953c192ccbb9d1d 100644
--- a/theories/heap_lang/wp_tactics.v
+++ b/theories/heap_lang/wp_tactics.v
@@ -1,4 +1,4 @@
-From iris.heap_lang Require Export tactics op_rules.
+From iris.heap_lang Require Export tactics lifting.
 Import uPred.
 
 (** wp-specific helper tactics *)