From 42ecd0a6c98be7d4d4a1b9adbfd61d18c339d12b Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 6 Aug 2017 18:47:47 +0200
Subject: [PATCH] Stronger delete_option_local_update

---
 theories/algebra/local_updates.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 7ea069d64..cdb86b1aa 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -166,9 +166,8 @@ Proof.
   destruct z as [z|]; last done. destruct y; inversion Heq.
 Qed.
 
-Lemma delete_option_local_update {A : cmraT} (x y : A) :
-  Exclusive y →
-  (Some x, Some y) ~l~> (None, None).
+Lemma delete_option_local_update {A : cmraT} (x : option A) (y : A) :
+  Exclusive y → (x, Some y) ~l~> (None, None).
 Proof.
   move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
   destruct z as [z|]; last done. exfalso.
-- 
GitLab