Fix bug in change_with_curried

Comes from unfortunate behavior of [change x with y in *]

1 files changed, 9 insertions, 1 deletions

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