diff --git a/theories/tactics.v b/theories/tactics.v
index 43155ebf220fdf1c147c28dee7990c90f3c4d9d0..bfc7815689d4362fadb8ad4607a3b3f271dc9eae 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -250,11 +250,13 @@ Ltac setoid_subst :=
   | H : @equiv ?A ?e _ ?x |- _ => symmetry in H; setoid_subst_aux (@equiv A e) x
   end.
 
-(** f_equiv works on goals of the form "f _ = f _", for any relation and any
-number of arguments. It looks for an appropriate "Proper" instance, and applies
+(** f_equiv works on goals of the form [f _ = f _], for any relation and any
+number of arguments. It looks for an appropriate [Proper] instance, and applies
 it. The tactic is somewhat limited, since it cannot be used to backtrack on
 the Proper instances that has been found. To that end, we try to ensure the
-trivial instance in which the resulting goals have an [eq]. *)
+trivial instance in which the resulting goals have an [eq]. More generally,
+when having [Proper (equiv ==> dist) f] and [Proper (dist ==> dist) f], it will
+favor the second. *)
 Ltac f_equiv :=
   match goal with
   | _ => reflexivity