From 173af5fba4489adcd975f425939714e80afa3892 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Tue, 31 May 2016 16:21:37 +0200
Subject: [PATCH] More documentation of f_equiv.
---
prelude/tactics.v | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/prelude/tactics.v b/prelude/tactics.v
index fabd259d..98c88fe9 100644
--- a/prelude/tactics.v
+++ b/prelude/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