From adfc72faca7c13cc64de189f6998d70c72df5309 Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Mon, 16 Nov 2015 16:05:05 +0100
Subject: [PATCH] Statement of ra_sep_ex.

---
 iris_core.v            | 5 ++---
 lib/ModuRes/RAConstr.v | 2 +-
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/iris_core.v b/iris_core.v
index 5e873a885..39a051e1c 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -201,9 +201,8 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
 
   Section Resources.
 
-    Lemma state_sep {σ g rf} (Hv : ↓(ex_own σ, g) · rf) : fst rf == 1 (ex_own σ)
-.
-    Proof. move: (ra_sep_prod Hv) => [Hs _]; exact: ra_sep_ex Hs. Qed.
+    Lemma state_sep {σ g rf} (Hv : ↓(ex_own σ, g) · rf) : fst rf == 1 (ex_own σ).
+    Proof. move: (ra_sep_prod Hv) => [Hs _]. by rewrite (ra_sep_ex Hs). Qed.
 
     Lemma state_fps {σ g σ' rf} (Hv : ↓(ex_own σ, g) · rf) : ↓(ex_own σ', g) · rf.
     Proof. exact: (ra_fps_fst (ra_fps_ex σ σ') rf). Qed.
diff --git a/lib/ModuRes/RAConstr.v b/lib/ModuRes/RAConstr.v
index b0c8cbefb..43b6fd4a4 100644
--- a/lib/ModuRes/RAConstr.v
+++ b/lib/ModuRes/RAConstr.v
@@ -73,7 +73,7 @@ Section Exclusive.
     - intros [t1| |] [t2| |]; unfold ra_valid; simpl; now auto.
   Qed.
 
-  Lemma ra_sep_ex {t r} : ↓ex_own t · r -> r == 1 r.
+  Lemma ra_sep_ex {t r} : ↓ex_own t · r -> r = 1 r.
   Proof. by case: r. Qed.
 
   Lemma ra_fps_ex_any t {r} (Hr : ↓r) : ex_own t ⇝ r.
-- 
GitLab