diff options
Diffstat (limited to 'plugins/ltac/taccoerce.mli')
| -rw-r--r-- | plugins/ltac/taccoerce.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 31bce197b..56f881684 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -11,7 +11,6 @@ open Util open Names open EConstr -open Misctypes open Genarg open Geninterp open Tactypes @@ -87,7 +86,7 @@ val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypo val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis -val coerce_to_int_or_var_list : Value.t -> int or_var list +val coerce_to_int_or_var_list : Value.t -> int Locus.or_var list (** {5 Missing generic arguments} *) |