diff --git a/theories/tactics.v b/theories/tactics.v
index f088b178f240e3af14a679a60f7088c2608844a2..dd49ea68ce8b786ffacd5b7b98fb50db2da65054 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -253,10 +253,11 @@ Ltac setoid_subst :=
 (** 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
+the Proper instances that has been found. To that end, we try to avoid the
 trivial instance in which the resulting goals have an [eq]. More generally,
+we try to "maintain" the relation of the current goal. For example,
 when having [Proper (equiv ==> dist) f] and [Proper (dist ==> dist) f], it will
-favor the second. *)
+favor the second because the relation (dist) stays the same. *)
 Ltac f_equiv :=
   match goal with
   | _ => reflexivity