Add [change_with_curried] to Curry.v

1 files changed, 14 insertions, 0 deletions

diff --git a/src/Util/Curry.v b/src/Util/Curry.v
index 0e1c0d635..fe92baa30 100644
--- a/src/Util/Curry.v
+++ b/src/Util/Curry.v
@@ -1,2 +1,16 @@
 Definition curry2 {A B C} (f : A -> B -> C) (x : A * B) : C
 := let '(a, b) := x in f a b.
+
+Ltac change_with_curried f :=
+  cbv beta in f; (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=5430 *)
+  lazymatch type of f with
+  | ?A -> ?B -> ?C
+    => let f' := fresh f in
+       rename f into f';
+       pose (fun (ab : A * B) => f' (fst ab) (snd ab)) as f;
+       change f' with (fun (a : A) (b : B) => f (a, b));
+       subst f';
+       cbv beta;
+       change_with_curried f
+  | _ => idtac
+  end.