From 34cb1f6491017e4ed1a509f6b83b88a812ac425f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 9 Dec 2014 12:09:44 +0100 Subject: Tentatively more informative report of failure when inferring pattern-matching predicate. --- pretyping/pretype_errors.mli | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'pretyping/pretype_errors.mli') diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 5882d8b9c..122240621 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -37,8 +37,7 @@ type pretype_error = | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (** Tactic Unification *) | UnifOccurCheck of existential_key * constr - | UnsolvableImplicit of Evd.evar_info * Evar_kinds.t * - Evd.unsolvability_explanation option + | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr @@ -100,7 +99,7 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b val error_unsolvable_implicit : - Loc.t -> env -> Evd.evar_map -> Evd.evar_info -> Evar_kinds.t -> + Loc.t -> env -> Evd.evar_map -> existential_key -> Evd.unsolvability_explanation option -> 'b val error_cannot_unify_loc : Loc.t -> env -> Evd.evar_map -> -- cgit v1.2.3