1 files changed, 10 insertions, 0 deletions
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))