diff --git a/theories/base.v b/theories/base.v
index a09cd676ff7b92e32dd709ab3e11fa3df9047aba..f8105fb370340d9d345f7bb22484d130e70b4742 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1468,6 +1468,8 @@ Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
   elem_of_elements (X : C) x : x ∈ elements X ↔ x ∈ X;
   NoDup_elements (X : C) : NoDup (elements X)
 }.
+Global Hint Mode FinSet - ! - - - - - - - - : typeclass_instances.
+
 Class Size C := size: C → nat.
 Global Hint Mode Size ! : typeclass_instances.
 Global Arguments size {_ _} !_ / : simpl nomatch, assert.