diff options
Diffstat (limited to 'plugins/ltac/taccoerce.mli')
| -rw-r--r-- | plugins/ltac/taccoerce.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 5185217cd..31bce197b 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -14,6 +14,7 @@ open EConstr open Misctypes open Genarg open Geninterp +open Tactypes (** Coercions from highest level generic arguments to actual data used by Ltac interpretation. Those functions examinate dynamic types and try to return @@ -56,7 +57,7 @@ val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr val coerce_to_intro_pattern_naming : - Environ.env -> Evd.evar_map -> Value.t -> intro_pattern_naming_expr + Environ.env -> Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr val coerce_to_hint_base : Value.t -> string |