From 3b8eed3c6cf6af9749c17b6a7f553054c664a55e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Sun, 30 Jun 2019 12:02:42 +0200
Subject: [PATCH] Fix bug in `solve_proper_prepare` to also handle unary
functions.
---
theories/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/tactics.v b/theories/tactics.v
index bd85e7f..4045a47 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -355,7 +355,7 @@ Ltac solve_proper_prepare :=
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
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
goal afterwards. *)
intros ?; intros
--
2.24.1