Add an Ltac1 to Ltac2 FFI for identifiers.

Before you ask, the Ltac2.Ltac1 module is voluntarily underdocumented.

Fixes #13996: missing Ltac1.to_ident.

2 files changed, 13 insertions, 0 deletions

diff --git a/user-contrib/Ltac2/Ltac1.v b/user-contrib/Ltac2/Ltac1.v
index fd1555c2fb..0f7167939b 100644
--- a/user-contrib/Ltac2/Ltac1.v
+++ b/user-contrib/Ltac2/Ltac1.v
@@ -40,5 +40,8 @@ Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "ltac2" "ltac1_ap
 Ltac2 @ external of_constr : constr -> t := "ltac2" "ltac1_of_constr".
 Ltac2 @ external to_constr : t -> constr option := "ltac2" "ltac1_to_constr".
 
+Ltac2 @ external of_ident : ident -> t := "ltac2" "ltac1_of_ident".
+Ltac2 @ external to_ident : t -> ident option := "ltac2" "ltac1_to_ident".
+
 Ltac2 @ external of_list : t list -> t := "ltac2" "ltac1_of_list".
 Ltac2 @ external to_list : t -> t list option := "ltac2" "ltac1_to_list".
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index fa7df5dfeb..457b8e1acf 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1186,6 +1186,16 @@ let () = define1 "ltac1_to_constr" ltac1 begin fun v ->
   return (Value.of_option Value.of_constr (Tacinterp.Value.to_constr v))
 end
 
+let () = define1 "ltac1_of_ident" ident begin fun c ->
+  let open Ltac_plugin in
+  return (Value.of_ext val_ltac1 (Taccoerce.Value.of_ident c))
+end
+
+let () = define1 "ltac1_to_ident" ltac1 begin fun v ->
+  let open Ltac_plugin in
+  return (Value.of_option Value.of_ident (Taccoerce.Value.to_ident v))
+end
+
 let () = define1 "ltac1_of_list" (list ltac1) begin fun l ->
   let open Geninterp.Val in
   return (Value.of_ext val_ltac1 (inject (Base typ_list) l))