From 315ef81d7b82d9787f17cb378b18d79cdd309dc8 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 30 May 2016 19:52:07 +0200
Subject: [PATCH] Simplify local update for excl

---
 algebra/excl.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/algebra/excl.v b/algebra/excl.v
index 5e83c0e59..c67a912fa 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -116,7 +116,7 @@ Proof. uPred.unseal. by destruct x. Qed.
 
 (** ** Local updates *)
 Global Instance excl_local_update y :
-  LocalUpdate (λ x, if x is Excl _ then ✓ y else False) (λ _, y).
+  LocalUpdate (λ _, True) (λ _, y).
 Proof. split. apply _. by destruct y; intros n [a|] [b'|]. Qed.
 
 (** Updates *)
-- 
GitLab