From 9bc0a38ba3f0cbf159348ba85f916fed64671a8b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 22 Oct 2016 12:52:19 +0200
Subject: [PATCH] Rename model -> iprop, ghost_ownership -> own.
---
_CoqProject | 4 ++--
heap_lang/heap.v | 2 +-
heap_lang/lib/barrier/protocol.v | 2 +-
program_logic/{model.v => iprop.v} | 0
program_logic/iris.v | 2 +-
program_logic/{ghost_ownership.v => own.v} | 2 +-
program_logic/saved_prop.v | 2 +-
7 files changed, 7 insertions(+), 7 deletions(-)
rename program_logic/{model.v => iprop.v} (100%)
rename program_logic/{ghost_ownership.v => own.v} (99%)
diff --git a/_CoqProject b/_CoqProject
index 54d3925c6..8d3655da7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -67,7 +67,7 @@ base_logic/big_op.v
base_logic/hlist.v
base_logic/soundness.v
base_logic/double_negation.v
-program_logic/model.v
+program_logic/iprop.v
program_logic/adequacy.v
program_logic/lifting.v
program_logic/invariants.v
@@ -80,7 +80,7 @@ program_logic/language.v
program_logic/ectx_language.v
program_logic/ectxi_language.v
program_logic/ectx_lifting.v
-program_logic/ghost_ownership.v
+program_logic/own.v
program_logic/saved_prop.v
program_logic/auth.v
program_logic/sts.v
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 9bf95350b..6cc7e1783 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -1,6 +1,6 @@
From iris.heap_lang Require Export lifting.
From iris.algebra Require Import auth gmap frac dec_agree.
-From iris.program_logic Require Export invariants ghost_ownership.
+From iris.program_logic Require Export invariants.
From iris.program_logic Require Import wsat auth.
From iris.proofmode Require Import tactics.
Import uPred.
diff --git a/heap_lang/lib/barrier/protocol.v b/heap_lang/lib/barrier/protocol.v
index 97258bf77..f59a64247 100644
--- a/heap_lang/lib/barrier/protocol.v
+++ b/heap_lang/lib/barrier/protocol.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export sts.
-From iris.program_logic Require Import ghost_ownership.
+From iris.program_logic Require Import own.
From iris.prelude Require Export gmap.
(** The STS describing the main barrier protocol. Every state has an index-set
diff --git a/program_logic/model.v b/program_logic/iprop.v
similarity index 100%
rename from program_logic/model.v
rename to program_logic/iprop.v
diff --git a/program_logic/iris.v b/program_logic/iris.v
index 17d827315..f0c91c294 100644
--- a/program_logic/iris.v
+++ b/program_logic/iris.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export ghost_ownership language.
+From iris.program_logic Require Export own language.
From iris.prelude Require Export coPset.
From iris.algebra Require Import gmap auth agree gset coPset.
diff --git a/program_logic/ghost_ownership.v b/program_logic/own.v
similarity index 99%
rename from program_logic/ghost_ownership.v
rename to program_logic/own.v
index 40c65ecd4..e29317bb2 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/own.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export model.
+From iris.program_logic Require Export iprop.
From iris.algebra Require Import iprod gmap.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import classes.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 235c246e3..5a804a2a1 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export ghost_ownership.
+From iris.program_logic Require Export own.
From iris.algebra Require Import agree.
From iris.prelude Require Import gmap.
Import uPred.
--
GitLab