From c2c98f80a46e0d2eb5aa4a7e8d2f8c696c2546cb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 29 Oct 2020 10:23:37 +0100
Subject: [PATCH] reduce TC assumptions made by fin_to_set

---
 theories/sets.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/sets.v b/theories/sets.v
index 5e1e72d6..b0522842 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -875,7 +875,7 @@ Section option_and_list_to_set.
 End option_and_list_to_set.
 
 (** * Finite types to sets. *)
-Definition fin_to_set (A : Type) `{SemiSet A C, Finite A} : C :=
+Definition fin_to_set (A : Type) `{Singleton A C, Empty C, Union C, Finite A} : C :=
   list_to_set (enum A).
 
 Section fin_to_set.
@@ -890,7 +890,6 @@ Section fin_to_set.
   Proof. constructor. split; auto using elem_of_fin_to_set. Qed.
 End fin_to_set.
 
-
 (** * Guard *)
 Global Instance set_guard `{MonadSet M} : MGuard M :=
   λ P dec A x, match dec with left H => x H | _ => ∅ end.
-- 
GitLab