From d7d3cacff8e5d18ec2cdaa7c6ed89c716c60ade6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 Feb 2016 20:53:08 +0100
Subject: [PATCH] prove that 'deleting' in the exclusive CMRA is a local update

---
 algebra/excl.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/algebra/excl.v b/algebra/excl.v
index cf50b1f71..e7023685c 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -143,6 +143,10 @@ Global Instance excl_local_update b :
   LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, Excl b).
 Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.
 
+Global Instance excl_local_update_del :
+LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, ExclUnit).
+Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.
+
 (** Updates *)
 Lemma excl_update (x : A) y : ✓ y → Excl x ~~> y.
 Proof. by destruct y; intros ? [?| |]. Qed.
-- 
GitLab