From 7b4018dc480826373f6295e1d68a6418279f1a0e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 24 Mar 2021 18:00:44 +0100
Subject: Add an Ltac1 to Ltac2 FFI for identifiers.

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

Fixes #13996: missing Ltac1.to_ident.
---
 plugins/ltac/taccoerce.ml  | 7 +++++++
 plugins/ltac/taccoerce.mli | 2 ++
 2 files changed, 9 insertions(+)

(limited to 'plugins')

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
-- 
cgit v1.2.3