diff --git a/_CoqProject b/_CoqProject
index 16f5ace4b13cee766be7a5a0fbdde8cfddac4b53..93bfbaacbc8883a1feb8f3a188ee2b15fa08a5c7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -96,7 +96,7 @@ program_logic/ownp.v
 heap_lang/lang.v
 heap_lang/tactics.v
 heap_lang/wp_tactics.v
-heap_lang/rules.v
+heap_lang/op_rules.v
 heap_lang/notation.v
 heap_lang/lib/spawn.v
 heap_lang/lib/par.v
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index a6a34384d2a86072401487b64d4c102db2b4589c..de6640d5ea55e1f7aaa613292d1b4fb3121f3cf4 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre adequacy gen_heap.
-From iris.heap_lang Require Export rules.
+From iris.heap_lang Require Export op_rules.
 From iris.algebra Require Import auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index e9d37f8ab0fc405759253601fb9de74459e32bbc..422f8d8b51330b4e505f6c281fef1078aa42a8fc 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -1,4 +1,4 @@
-From iris.heap_lang Require Export rules notation.
+From iris.heap_lang Require Export op_rules notation.
 From iris.base_logic.lib Require Export invariants.
 
 Structure lock Σ `{!heapG Σ} := Lock {
diff --git a/heap_lang/rules.v b/heap_lang/op_rules.v
similarity index 99%
rename from heap_lang/rules.v
rename to heap_lang/op_rules.v
index e851f42d6a5f5c8fae0e656c8df7b123fa55a363..55b665f43a982f3e71ccefe7c7520f6f1a4f9f4d 100644
--- a/heap_lang/rules.v
+++ b/heap_lang/op_rules.v
@@ -6,6 +6,8 @@ From iris.proofmode Require Import tactics.
 From iris.prelude Require Import fin_maps.
 Import uPred.
 
+(** Basic rules for language operations. *)
+
 Class heapG Σ := HeapG {
   heapG_invG : invG Σ;
   heapG_gen_heapG :> gen_heapG loc val Σ
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 08ae37f7937daff6827f3c9131907f60fb6bba34..acee4c4ec0d7328e437b05ef4175fed1feaf30fe 100644
--- a/heap_lang/proofmode.v
+++ b/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 rules.
+From iris.heap_lang Require Export wp_tactics op_rules.
 Import uPred.
 
 Ltac wp_strip_later ::= iNext.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 85c1e30b98ca8103da0c0045a08cca5c4dde4ed3..d7cf79c912f5341e749a2c31ffc2efe48fd33b7f 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -1,4 +1,4 @@
-From iris.heap_lang Require Export tactics rules.
+From iris.heap_lang Require Export tactics op_rules.
 Import uPred.
 
 (** wp-specific helper tactics *)