Skip to content
Snippets Groups Projects
Commit ba3c17be authored by Ralf Jung's avatar Ralf Jung
Browse files

make sure this solves the goal

parent 6aa72baa
Branches
Tags
1 merge request!428Tweak `f_equiv` to use `reflexivity` in a way similar to `f_equal`.
Pipeline #74820 canceled
......@@ -364,7 +364,7 @@ Ltac setoid_subst :=
be used to avoid expensive failing unification. *)
Ltac fast_reflexivity :=
match goal with
| |- _ ?x ?x => simple apply reflexivity
| |- _ ?x ?x => solve [simple apply reflexivity]
end.
(** f_equiv works on goals of the form [f _ = f _], for any relation and any
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment