Ltac2: Take some small APIs from rewriter (fst/snd, Special chars)

user-contrib/Ltac2/Char.v

@@ -16,3 +16,13 @@ Ltac2 @external to_int : char -> int := "coq-core.plugins.ltac2" "char_to_int".
 
 Ltac2 equal (x : char) (y : char) : bool := Int.equal (to_int x) (to_int y).
 Ltac2 compare (x : char) (y : char) : int := Int.compare (to_int x) (to_int y).
+
+(** Special characters *)
+Ltac2 null () : char := Char.of_int 0.
+Ltac2 backspace () : char := Char.of_int 8.
+Ltac2 tab () : char := Char.of_int 9.
+Ltac2 lf () : char := Char.of_int 10.
+Ltac2 newpage () : char := Char.of_int 12.
+Ltac2 cr () : char := Char.of_int 13.
+Ltac2 escape () : char := Char.of_int 27.
+Ltac2 newline () : char := Char.of_int 10.

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

user-contrib/Ltac2/String.v

@@ -9,6 +9,7 @@
 (************************************************************************)
 
 Require Import Ltac2.Init.
+Require Ltac2.Char.
 
 Ltac2 Type t := string.
 
@@ -22,3 +23,13 @@ Ltac2 @external equal : string -> string -> bool := "coq-core.plugins.ltac2" "st
 Ltac2 @external compare : string -> string -> int := "coq-core.plugins.ltac2" "string_compare".
 
 Ltac2 is_empty s := match s with "" => true | _ => false end.
+
+(** Special characters *)
+Ltac2 null () : string := String.make 1 (Char.null ()).
+Ltac2 backspace () : string := String.make 1 (Char.backspace ()).
+Ltac2 tab () : string := String.make 1 (Char.tab ()).
+Ltac2 lf () : string := String.make 1 (Char.lf ()).
+Ltac2 newpage () : string := String.make 1 (Char.newpage ()).
+Ltac2 cr () : string := String.make 1 (Char.cr ()).
+Ltac2 escape () : string := String.make 1 (Char.escape ()).
+Ltac2 newline () : string := String.make 1 (Char.newline ()).