diff --git a/theories/base.v b/theories/base.v
index fb129db3dda95ff55f794e2deaa66b9d210dfd6f..1a1473881e596470b363d140b0b68df4ff4a1f14 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -482,6 +482,11 @@ Definition curry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D :=
 Definition curry4 {A B C D E} (f : A → B → C → D → E) (p : A * B * C * D) : E :=
   let '(a,b,c,d) := p in f a b c d.
 
+Definition uncurry3 {A B C D} (f : A * B * C → D) (a : A) (b : B) (c : C) : D :=
+  f (a, b, c).
+Definition uncurry4 {A B C D E} (f : A * B * C * D → E)
+  (a : A) (b : B) (c : C) (d : D) : E := f (a, b, c, d).
+
 Definition prod_map {A A' B B'} (f: A → A') (g: B → B') (p : A * B) : A' * B' :=
   (f (p.1), g (p.2)).
 Arguments prod_map {_ _ _ _} _ _ !_ / : assert.