diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-09 12:09:44 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-11 18:34:04 +0100 |
| commit | 34cb1f6491017e4ed1a509f6b83b88a812ac425f (patch) | |
| tree | 0ad12f25af3050bb289147c54fe52f7349f2335e /pretyping/pretype_errors.mli | |
| parent | d083200ae5b391ceffaa0329a8e3a334036c7968 (diff) | |
Tentatively more informative report of failure when inferring
pattern-matching predicate.
Diffstat (limited to 'pretyping/pretype_errors.mli')
| -rw-r--r-- | pretyping/pretype_errors.mli | 5 |
1 files changed, 2 insertions, 3 deletions
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 -> |