diff --git a/theories/collections.v b/theories/collections.v
index 16a265daf3ddca3988fb1432a67bd656b53adeb8..1f40491968f1c562d0d7bc747a99cfc74d0a9a3a 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -140,7 +140,7 @@ Hint Mode SetUnfold + - : typeclass_instances.
 Class SetUnfoldSimpl (P Q : Prop) := { set_unfold_simpl : SetUnfold P Q }.
 Hint Extern 0 (SetUnfoldSimpl _ _) => csimpl; constructor : typeclass_instances.
 
-Instance set_unfold_fallthrough P : SetUnfold P P | 1000. done. Qed.
+Instance set_unfold_default P : SetUnfold P P | 1000. done. Qed.
 Definition set_unfold_1 `{SetUnfold P Q} : P → Q := proj1 (set_unfold P Q).
 Definition set_unfold_2 `{SetUnfold P Q} : Q → P := proj2 (set_unfold P Q).