Commit e1c92aa2 authored by Ralf Jung's avatar Ralf Jung

remove a useless try

parent b8ba5d8a
......@@ -345,7 +345,7 @@ Ltac solve_proper_prepare :=
| |- Proper _ _ => intros ???
| |- (_ ==> _)%signature _ _ => intros ???
| |- pointwise_relation _ _ _ _ => intros ?
| |- ?R ?f _ => try let f' := constr:(λ x, f x) in intros ?
| |- ?R ?f _ => let f' := constr:(λ x, f x) in intros ?
end; simplify_eq;
(* We try with and without unfolding. We have to backtrack on
that because unfolding may succeed, but then the proof may fail. *)
......
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