From 7b14d6a72742eb7913fce8ab5d2d297359ae5ab9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 9 Dec 2016 23:22:20 +0100
Subject: [PATCH] rename rules -> op_rules

Really, *all* of our files contain proof rules
---
 _CoqProject                       | 2 +-
 heap_lang/adequacy.v              | 2 +-
 heap_lang/lib/lock.v              | 2 +-
 heap_lang/{rules.v => op_rules.v} | 2 ++
 heap_lang/proofmode.v             | 2 +-
 heap_lang/wp_tactics.v            | 2 +-
 6 files changed, 7 insertions(+), 5 deletions(-)
 rename heap_lang/{rules.v => op_rules.v} (99%)

diff --git a/_CoqProject b/_CoqProject
index 16f5ace4b..93bfbaacb 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 a6a34384d..de6640d5e 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 e9d37f8ab..422f8d8b5 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 e851f42d6..55b665f43 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 08ae37f79..acee4c4ec 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 85c1e30b9..d7cf79c91 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 *)
-- 
GitLab