Merge PR coq#18370: Ltac2: Take some small APIs from rewriter (fst/snd)

Reviewed-by: ppedrot Co-authored-by: ppedrot <[email protected]>
SkySkimmer · Jan 30, 2024 · 18b537d · 18b537d
2 parents a6d226f + be1bbe2
commit 18b537d
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 0 deletions.
diff --git a/doc/changelog/06-Ltac2-language/18370-ltac2-apis.rst b/doc/changelog/06-Ltac2-language/18370-ltac2-apis.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  `fst` and `snd` in `Ltac2.Init`
+  (`#18370 <https://github.com/coq/coq/pull/18370>`_,
+  by Gaëtan Gilbert).
diff --git a/test-suite/output/ltac2_printabout.out b/test-suite/output/ltac2_printabout.out
@@ -1,3 +1,5 @@
+fst : 'a * 'b -> 'a
+snd : 'b * 'a -> 'a
 type : constr -> constr
 Ltac2 type : constr -> constr
       type := @external "coq-core.plugins.ltac2" "constr_type"

diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
@@ -42,6 +42,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) ].