Merge PR #13997: Add an Ltac1 to Ltac2 FFI for identifiers.

Reviewed-by: MSoegtropIMC

5 files changed, 27 insertions, 0 deletions

diff --git a/doc/changelog/05-tactic-language/13997-ltac2-ident-ffi.rst b/doc/changelog/05-tactic-language/13997-ltac2-ident-ffi.rst
new file mode 100644
index 0000000000..b5b63455c9
--- /dev/null
+++ b/doc/changelog/05-tactic-language/13997-ltac2-ident-ffi.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Added a FFI to convert between Ltac1 and Ltac2 identifiers
+  (`#13997 <https://github.com/coq/coq/pull/13997>`_,
+  fixes `#13996 <https://github.com/coq/coq/issues/13996>`_,
+  by Pierre-Marie Pédrot).
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 5e88bf7c79..f2f5fc16a6 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -91,6 +91,13 @@ let to_int v =
     Some (out_gen (topwit wit_int) v)
   else None
 
+let of_ident id = in_gen (topwit wit_ident) id
+
+let to_ident v =
+  if has_type v (topwit wit_ident) then
+    Some (out_gen (topwit wit_ident) v)
+  else None
+
 let to_list v = prj Val.typ_list v
 
 let to_option v = prj Val.typ_opt v
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 8ca2510459..c748fb3d1a 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -39,6 +39,8 @@ sig
   val to_uconstr : t -> Ltac_pretype.closed_glob_constr option
   val of_int : int -> t
   val to_int : t -> int option
+  val of_ident : Id.t -> t
+  val to_ident : t -> Id.t option
   val to_list : t -> t list option
   val to_option : t -> t option option
   val to_pair : t -> (t * t) option
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))