aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Curry.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/Curry.v')
-rw-r--r--src/Util/Curry.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/Curry.v b/src/Util/Curry.v
index c06c3493d..0e1c0d635 100644
--- a/src/Util/Curry.v
+++ b/src/Util/Curry.v
@@ -1,2 +1,2 @@
Definition curry2 {A B C} (f : A -> B -> C) (x : A * B) : C
-:= f (fst x) (snd x).
+:= let '(a, b) := x in f a b.