From 63d057dd4b4eb2c73de2a2f8aa6fe8bb3613053a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Feb 2016 02:27:14 +0100
Subject: [PATCH] Rename heap_lang/heap_lang_tactics.v -> heap_lang/tactics.v
---
_CoqProject | 2 +-
heap_lang/lifting.v | 2 +-
heap_lang/{heap_lang_tactics.v => tactics.v} | 0
heap_lang/tests.v | 2 +-
4 files changed, 3 insertions(+), 3 deletions(-)
rename heap_lang/{heap_lang_tactics.v => tactics.v} (100%)
diff --git a/_CoqProject b/_CoqProject
index 354725716..a3165e834 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 7de00c2cb..4c643b9a7 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 444172f6a..97f4a4678 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.
--
GitLab