reduce TC assumptions made by fin_to_set

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.