rename program_logic.{ownership -> wsat}. It really is about world...

rename program_logic.{ownership -> wsat}. It really is about world satisfaction and invariants more than about ownership.

_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

heap_lang/adequacy.v

 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.
 

heap_lang/heap.v

 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

heap_lang/lifting.v

 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.

program_logic/adequacy.v

 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.
 

program_logic/ectx_lifting.v

 (** 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.

program_logic/invariants.v

 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.

program_logic/lifting.v

 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.
 

program_logic/pviewshifts.v

 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.

program_logic/weakestpre.v

 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.

tests/atomic.v

-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).

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.