diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
index 55b4cf65212d7..63632b6ac6bd6 100644
--- a/user-contrib/Ltac2/Init.v
+++ b/user-contrib/Ltac2/Init.v
@@ -41,6 +41,11 @@ Ltac2 Type ('a, 'b, 'c, 'd) format.
 Ltac2 Type exn := [ .. ].
 Ltac2 Type 'a array.
 
+(** Tuples *)
+
+Ltac2 fst (p:'a * 'b) : 'a := let (x,_) := p in x.
+Ltac2 snd (p:'a * 'b) : 'b := let (_,y) := p in y.
+
 (** Pervasive types *)
 
 Ltac2 Type 'a option := [ None | Some ('a) ].