From 49a61c0d51e969f5510bad99e2fe2ee15b798644 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 May 2016 16:21:37 +0200
Subject: [PATCH] More documentation of f_equiv.

---
 theories/tactics.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 43155ebf..bfc78156 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
-- 
GitLab