From 85b06738b30a0f85b332d877b169eca44bf0257c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 27 Feb 2019 10:58:48 +0100
Subject: [PATCH] doc introduction for ownp

---
 theories/program_logic/ownp.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 9e20b1a11..17530e77e 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -5,6 +5,15 @@ From iris.algebra Require Import auth.
 From iris.proofmode Require Import tactics classes.
 Set Default Proof Using "Type".
 
+(**
+This module provides an interface to handling ownership of the global state that
+works more like Iris 2.0 did.  The state interpretation (in WP) is fixed to be
+authoritative ownership of the entire state (using the [excl] RA).  Users can
+then put the corresponding fragment into an invariant on their own to establish
+a more interesting notion of ownership, such as the standard heap with disjoint
+union.
+*)
+
 Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
   ownP_invG : invG Σ;
   ownP_inG :> inG Σ (authR (optionUR (exclR (stateC Λ))));
-- 
GitLab