Commit 3b8eed3c authored by Robbert Krebbers's avatar Robbert Krebbers

Fix bug in `solve_proper_prepare` to also handle unary functions.

parent ff0750f5
...@@ -355,7 +355,7 @@ Ltac solve_proper_prepare := ...@@ -355,7 +355,7 @@ Ltac solve_proper_prepare :=
show up in the goal. To check that we actually have an equivalence relation show up in the goal. To check that we actually have an equivalence relation
on functions, we try to eta expand [f], which will only succeed if [f] is on functions, we try to eta expand [f], which will only succeed if [f] is
actually a function. *) actually a function. *)
let f' := constr:(λ x y, f x y) in let f' := constr:(λ x, f x) in
(* Now forcefully introduce the first ∀ and other ∀s that show up in the (* Now forcefully introduce the first ∀ and other ∀s that show up in the
goal afterwards. *) goal afterwards. *)
intros ?; intros intros ?; intros
......
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