diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-05 02:43:56 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-05 02:43:56 -0400 |
| commit | 3125b2c088cb33d5b029e74a7b938e25afc9a304 (patch) | |
| tree | 6c9a0c282dabb0966e4f7e7438712eae77c4c7b3 /src/Util/Curry.v | |
| parent | 8879a13f2972c98e86044f9961d0dcb696e44d30 (diff) | |
When currying, change with curried form in *
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 |