From 4485ef7d19e1a55c836245ba51c41c88610a22a1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 12 Oct 2016 14:05:27 +0200
Subject: [PATCH] rename program_logic.{ownership -> wsat}. It really is about
 world satisfaction and invariants more than about ownership.

---
 _CoqProject                           | 2 +-
 heap_lang/adequacy.v                  | 2 +-
 heap_lang/heap.v                      | 2 +-
 heap_lang/lifting.v                   | 2 +-
 program_logic/adequacy.v              | 2 +-
 program_logic/ectx_lifting.v          | 2 +-
 program_logic/invariants.v            | 2 +-
 program_logic/lifting.v               | 2 +-
 program_logic/pviewshifts.v           | 2 +-
 program_logic/weakestpre.v            | 2 +-
 program_logic/{ownership.v => wsat.v} | 0
 tests/atomic.v                        | 5 +++--
 tests/heap_lang.v                     | 2 +-
 13 files changed, 14 insertions(+), 13 deletions(-)
 rename program_logic/{ownership.v => wsat.v} (100%)

diff --git a/_CoqProject b/_CoqProject
index 6f18679ed..a38123baa 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -67,7 +67,7 @@ program_logic/model.v
 program_logic/adequacy.v
 program_logic/lifting.v
 program_logic/invariants.v
-program_logic/ownership.v
+program_logic/wsat.v
 program_logic/weakestpre.v
 program_logic/pviewshifts.v
 program_logic/hoare.v
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index 6da24be01..c6e482cba 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Export heap.
 From iris.algebra Require Import auth.
-From iris.program_logic Require Import ownership auth.
+From iris.program_logic Require Import wsat auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
 
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 8f0880623..5701bd313 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -1,7 +1,7 @@
 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 Import ownership auth.
+From iris.program_logic Require Import wsat auth.
 From iris.proofmode Require Import tactics.
 Import uPred.
 (* TODO: The entire construction could be generalized to arbitrary languages that have
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 278165adb..917c00025 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *)
+From iris.program_logic Require Import wsat ectx_lifting. (* for ownP *)
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 4b6540a71..96377473f 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.proofmode Require Import tactics.
 Import uPred.
 
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index b43ead95e..7d329558b 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -1,6 +1,6 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.proofmode Require Import tactics.
 
 Section wp.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 08b7407ae..8fe284f24 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export pviewshifts.
 From iris.program_logic Require Export namespaces.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.proofmode Require Import tactics coq_tactics intro_patterns.
 Import uPred.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index da791e981..b5f273237 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.algebra Require Export upred_big_op.
 From iris.proofmode Require Import tactics.
 
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index cf2070e49..2f6fb5c0a 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export iris.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.algebra Require Import upred_big_op gmap.
 From iris.proofmode Require Import tactics classes.
 Import uPred.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 9c8d93f85..0e8244c0b 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export pviewshifts.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.algebra Require Import upred_big_op.
 From iris.prelude Require Export coPset.
 From iris.proofmode Require Import tactics classes.
diff --git a/program_logic/ownership.v b/program_logic/wsat.v
similarity index 100%
rename from program_logic/ownership.v
rename to program_logic/wsat.v
diff --git a/tests/atomic.v b/tests/atomic.v
index 0b978bab8..72d20913d 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export hoare weakestpre pviewshifts ownership.
+From iris.program_logic Require Export hoare weakestpre pviewshifts.
 From iris.algebra Require Import upred_big_op.
 From iris.prelude Require Export coPset.
 From iris.proofmode Require Import tactics.
@@ -41,7 +41,9 @@ Section atomic.
   Arguments atomic_triple {_} _ _ _ _.
 End atomic.
 
+(* TODO: Importing in the middle of the file is bad practice. *)
 From iris.heap_lang Require Export lang proofmode notation.
+From iris.heap_lang.lib Require Import par.
 
 Section incr.
   Context `{!heapG Σ} (N : namespace).
@@ -92,7 +94,6 @@ Section incr.
   Qed.
 End incr.
 
-From iris.heap_lang.lib Require Import par.
 
 Section user.
   Context `{!heapG Σ, !spawnG Σ} (N : namespace).
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 3a1a31fd2..bccc4848c 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -2,7 +2,7 @@
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import adequacy.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.heap_lang Require Import proofmode notation.
 
 Section LiftingTests.
-- 
GitLab