From 78f10027af0dd86b0dbb4aec18b6976e930853f5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 12 Dec 2016 10:47:27 +0100
Subject: [PATCH] rename op_rules -> lifting

---
 _CoqProject                                  | 2 +-
 theories/heap_lang/adequacy.v                | 2 +-
 theories/heap_lang/{op_rules.v => lifting.v} | 4 ++--
 theories/heap_lang/proofmode.v               | 2 +-
 theories/heap_lang/wp_tactics.v              | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)
 rename theories/heap_lang/{op_rules.v => lifting.v} (99%)

diff --git a/_CoqProject b/_CoqProject
index 1332a4ef0..c075b17c6 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 de6640d5e..295fe6a8a 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 55b665f43..807ae26b5 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 acee4c4ec..e0465a37a 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 d7cf79c91..16e01deef 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 *)
-- 
GitLab