diff options
| author | Michael Soegtrop | 2021-03-30 00:21:48 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2021-03-30 00:21:48 +0200 |
| commit | 303afeab9c946bdba15e1984231ae5066bf37af6 (patch) | |
| tree | 1b5abc950274c925271df959a5fd85dca921c02f /plugins | |
| parent | c6e9b36f2abc7bf434df8e9a6fea48ba9db4efc0 (diff) | |
| parent | 529243826c3a51ca0bc6d37cf0f1d3c697b8a3e9 (diff) | |
Merge PR #13997: Add an Ltac1 to Ltac2 FFI for identifiers.
Reviewed-by: MSoegtropIMC
Diffstat (limited to 'plugins')
| -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 |