diff options
Diffstat (limited to 'plugins/ltac/taccoerce.mli')
| -rw-r--r-- | plugins/ltac/taccoerce.mli | 2 |
1 files changed, 2 insertions, 0 deletions
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 |