diff --git a/theory/rationals.v b/theory/rationals.v
index 4449d45..1e00909 100644
--- a/theory/rationals.v
+++ b/theory/rationals.v
@@ -85,6 +85,8 @@ Hint Unfold rationals_to_rationals : typeclass_instances.
 Section another_rationals.
   Context `{Rationals Q1} `{Rationals Q2}.
 
+  Hint Extern 4 => progress unfold rationals_to_rationals : typeclass_instances.
+
   Local Existing Instance to_frac_bijective.
   Global Instance: SemiRing_Morphism (rationals_to_rationals Q1 Q2) := _.
   Global Instance: Bijective (rationals_to_rationals Q1 Q2) := _.
@@ -142,7 +144,7 @@ Section isomorphic_image_is_rationals.
   Context (f : Q → F) `{!Inverse f} `{!Bijective f} `{!SemiRing_Morphism f}.
 
   Instance iso_to_frac: RationalsToFrac F := λ Z _ _ _ _ _ _ _ _, rationals_to_frac Q Z ∘ f⁻¹.
-  Hint Unfold iso_to_frac: typeclass_instances.
+  Hint Extern 4 => progress unfold iso_to_frac : typeclass_instances.
 
   Instance: Bijective (f⁻¹) := _.
   Instance: SemiRing_Morphism (f⁻¹) := {}.
diff --git a/theory/ua_subalgebra.v b/theory/ua_subalgebra.v
index 9d30d6e..5e3d0ff 100644
--- a/theory/ua_subalgebra.v
+++ b/theory/ua_subalgebra.v
@@ -36,7 +36,7 @@ Section subalgebras.
 
   Definition carrier s := sig (P s).
 
-  Hint Unfold carrier: typeclass_instances.
+  Hint Extern 4 => progress unfold carrier: typeclass_instances.
 
   (* We can implement closed operations in the new algebra: *)
 
diff --git a/theory/ua_subalgebraT.v b/theory/ua_subalgebraT.v
index b1a824e..51ec38f 100644
--- a/theory/ua_subalgebraT.v
+++ b/theory/ua_subalgebraT.v
@@ -46,7 +46,7 @@ Section subalgebras.
 
   Definition carrier s := sigT (P s).
 
-  Hint Unfold carrier: typeclass_instances.
+  Hint Extern 4 => progress unfold carrier: typeclass_instances.
 
   (* We can implement closed operations in the new algebra: *)
 
@@ -78,4 +78,4 @@ Section subalgebras.
   Proof. constructor. apply _. intro. apply close_op_proper, algebra_propers. Qed.
 End subalgebras.
 
-Hint Unfold carrier: typeclass_instances.
+Hint Extern 4 => progress unfold carrier: typeclass_instances.