From 22d4a0cd8bdbba4f94aa8b95272d527bc6553795 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Feb 2019 13:27:42 +0100
Subject: [PATCH] =?UTF-8?q?=E2=88=88=20on=20`listset`=20is=20decidable.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/listset.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/theories/listset.v b/theories/listset.v
index 23ac7c38..0d864ce8 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -38,7 +38,12 @@ Proof.
   abstract (by rewrite listset_empty_alt).
 Defined.
 
-Context `{!EqDecision A}.
+Context `{Aeq : !EqDecision A}.
+
+Global Instance listset_elem_of_dec : RelDecision (∈@{listset A}).
+Proof using Aeq.
+  refine (λ x X, cast_if (decide (x ∈ listset_car X))); done.
+Defined.
 
 Global Instance listset_intersection: Intersection (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (list_intersection l' k').
-- 
GitLab