diff --git a/_CoqProject b/_CoqProject
index 354725716141a2836952ad39c47150f1b37ec0e1..a3165e834e7238bfecef76b8948e63bb42f31765 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -67,7 +67,7 @@ program_logic/tests.v
 program_logic/auth.v
 program_logic/ghost_ownership.v
 heap_lang/heap_lang.v
-heap_lang/heap_lang_tactics.v
+heap_lang/tactics.v
 heap_lang/lifting.v
 heap_lang/derived.v
 heap_lang/notation.v
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 7de00c2cbdcda6859ea2ac2f3cdc6f70020d7906..4c643b9a74f8d26d1444ce7f1e3f4e255da538d9 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,7 +1,7 @@
 Require Export program_logic.weakestpre heap_lang.heap_lang.
 Require Import program_logic.lifting.
 Require Import program_logic.ownership. (* for ownP *)
-Require Import heap_lang.heap_lang_tactics.
+Require Import heap_lang.tactics.
 Export heap_lang. (* Prefer heap_lang names over language names. *)
 Import uPred.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
diff --git a/heap_lang/heap_lang_tactics.v b/heap_lang/tactics.v
similarity index 100%
rename from heap_lang/heap_lang_tactics.v
rename to heap_lang/tactics.v
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 444172f6a48c67c68bbbf47db1efe2bc49c2d377..97f4a4678d8829719998386e6812140ac95ed923 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -1,6 +1,6 @@
 (** This file is essentially a bunch of testcases. *)
 Require Import program_logic.ownership.
-Require Import heap_lang.notation heap_lang.substitution heap_lang.heap_lang_tactics.
+Require Import heap_lang.notation heap_lang.substitution heap_lang.tactics.
 Import uPred.
 
 Module LangTests.