diff --git a/prelude/tactics.v b/prelude/tactics.v
index dd46cd809fa5c9a1c4b616179d0a8015cd1fc005..9e70ba94a458219a1fc9f641c37e686f6357dbed 100644
--- a/prelude/tactics.v
+++ b/prelude/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