From 3125b2c088cb33d5b029e74a7b938e25afc9a304 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 5 Apr 2017 02:43:56 -0400
Subject: When currying, change with curried form in *

---
 src/Util/Curry.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/Util/Curry.v')

diff --git a/src/Util/Curry.v b/src/Util/Curry.v
index fe92baa30..6d15eca05 100644
--- a/src/Util/Curry.v
+++ b/src/Util/Curry.v
@@ -8,7 +8,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));
+       change f' with (fun (a : A) (b : B) => f (a, b)) in *;
        subst f';
        cbv beta;
        change_with_curried f
-- 
cgit v1.2.3