diff options
| author | Pierre-Marie Pédrot | 2021-03-24 18:00:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-26 15:51:08 +0100 |
| commit | 7b4018dc480826373f6295e1d68a6418279f1a0e (patch) | |
| tree | 2dca07494d2cd8d43e8a8c42354e6f51e98c332b /plugins/ltac | |
| parent | c2ed2e395f2164ebbc550e70899c49af23e1ad1e (diff) | |
Add an Ltac1 to Ltac2 FFI for identifiers.
Before you ask, the Ltac2.Ltac1 module is voluntarily underdocumented.
Fixes #13996: missing Ltac1.to_ident.
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 7 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.mli | 2 |
2 files changed, 9 insertions, 0 deletions
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 |