From 24067eaab4113f1a7568bd5867c6e208a49e00be Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 5 Dec 2023 15:57:20 +0100
Subject: [PATCH] Ltac2: Take some small APIs from rewriter (fst/snd)

---
 user-contrib/Ltac2/Init.v | 5 +++++
 1 file changed, 5 insertions(+)

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) ].