From 45b28c125c63fe0f41cd2a14c5f5e8b536962a42 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Feb 2016 16:09:06 +0100
Subject: [PATCH] Frame preserving updates for excl.

---
 modures/excl.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/modures/excl.v b/modures/excl.v
index 795c2840d..341e7b27a 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -142,6 +142,8 @@ Qed.
 (* Updates *)
 Lemma excl_update (x : A) y : ✓ y → Excl x ⇝ y.
 Proof. by destruct y; intros ? [?| |]. Qed.
+Lemma excl_updateP (P : excl A → Prop) x y : ✓ y → P y → Excl x ⇝: P.
+Proof. intros ?? z n ?; exists y. by destruct y, z as [?| |]. Qed.
 End excl.
 
 Arguments exclC : clear implicits.
-- 
GitLab