Commit 4653cb6d authored by Ralf Jung's avatar Ralf Jung

improve f_equiv doc

parent 39b9a3c5
Pipeline #2906 passed with stage
in 9 minutes and 26 seconds
...@@ -253,10 +253,11 @@ Ltac setoid_subst := ...@@ -253,10 +253,11 @@ Ltac setoid_subst :=
(** f_equiv works on goals of the form [f _ = f _], for any relation and any (** 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 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 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, 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 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 := Ltac f_equiv :=
match goal with match goal with
| _ => reflexivity | _ => reflexivity
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment