diff options
Diffstat (limited to 'src/Util/Curry.v')
| -rw-r--r-- | src/Util/Curry.v | 2 |
1 files changed, 1 insertions, 1 deletions
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 |