diff --git a/theories/sets.v b/theories/sets.v
index 5e1e72d6595a2c005626b16b03aa9c291629b301..b0522842a41ba2412de3fba4e0df0defab50e871 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.