From fa5c6aed76360c188ac097259b774ba32129aecb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 5 Apr 2017 02:49:36 -0400 Subject: Fix bug in change_with_curried Comes from unfortunate behavior of [change x with y in *] --- src/Util/Curry.v | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'src/Util/Curry.v') diff --git a/src/Util/Curry.v b/src/Util/Curry.v index 6d15eca05..8a34cb611 100644 --- a/src/Util/Curry.v +++ b/src/Util/Curry.v @@ -1,6 +1,14 @@ Definition curry2 {A B C} (f : A -> B -> C) (x : A * B) : C := let '(a, b) := x in f a b. +(** Work around "Cannot create self-referring hypothesis" coming from + [change x with y in *] *) +Local Ltac change_in_all from to := + change from with to; + repeat match goal with + | [ H : _ |- _ ] => progress change from with to in H + end. + 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 @@ -8,7 +16,7 @@ Ltac change_with_curried f := => 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)) in *; + change_in_all f' (fun (a : A) (b : B) => f (a, b)); subst f'; cbv beta; change_with_curried f -- cgit v1.2.3