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.ml | |
| parent | d083200ae5b391ceffaa0329a8e3a334036c7968 (diff) | |
Tentatively more informative report of failure when inferring
pattern-matching predicate.
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 99b5a51f9..9b5b79284 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -36,8 +36,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 @@ -107,9 +106,9 @@ let error_not_a_type_loc loc env sigma j = let error_occur_check env sigma ev c = raise (PretypeError (env, sigma, UnifOccurCheck (ev,c))) -let error_unsolvable_implicit loc env sigma evi e explain = +let error_unsolvable_implicit loc env sigma evk explain = Loc.raise loc - (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain))) + (PretypeError (env, sigma, UnsolvableImplicit (evk, explain))) let error_cannot_unify_loc loc env sigma ?reason (m,n) = Loc.raise loc (PretypeError (env, sigma,CannotUnify (m,n,reason))) |