From 5c33aedd7b2f8f9e87ab210fcc764949109dd4bb Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Thu, 26 Feb 2015 14:39:39 +0100
Subject: [PATCH] Weaken res_sat: We'll always keep a physical state around.

---
 iris_plog.v      | 6 +-----
 lib/ModuRes/RA.v | 2 +-
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/iris_plog.v b/iris_plog.v
index 99236e0c2..2195dbe6e 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -102,11 +102,7 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
     Qed.
 
     (* When is a resource okay with a state? *)
-    Definition res_sat (r: res) σ: Prop := ↓r /\
-      match fst r with
-        | ex_own s => s = σ
-        | _ => True (* We don't care. Note that validity is ensured by the first conjunct. *)
-      end.
+    Definition res_sat (r: res) σ: Prop := ↓r /\ fst r == ex_own state σ.
 
     Global Instance res_sat_dist : Proper (equiv ==> equiv ==> iff) res_sat.
     Proof.
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index 1b88f573c..458211d93 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -1,4 +1,4 @@
-(** Resource algebras: Commutative monoids with a decidable validity predicate. *)
+(** Resource algebras: Commutative monoids with a validity predicate. *)
 
 Require Import Bool.
 Require Import Predom.
-- 
GitLab