diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-17 07:33:24 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-17 07:33:24 +0000 |
| commit | 90899bd52f32ef608754f937c5b23d250dc41ed8 (patch) | |
| tree | 9d7e0092b4b3dc1d099b6f0610eaf69b00401019 /pretyping/typeclasses_errors.ml | |
| parent | 21c8f5d0b74e72f61a086d92660d25ce35c482b7 (diff) | |
Better typeclass error messages, always giving the full set of
unsatisfiable constraints.
Add a resolution call in tacinterp before trying the default tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11131 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
| -rw-r--r-- | pretyping/typeclasses_errors.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 72d23946c..090776018 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -49,6 +49,7 @@ let unsatisfiable_constraints env evd ev = | Some ev -> let evi = Evd.find (Evd.evars_of evd) ev in let loc, kind = Evd.evar_source ev evd in - raise (Stdpp.Exc_located (loc, TypeClassError (env, UnsatisfiableConstraints (evd, Some (evi, kind))))) + raise (Stdpp.Exc_located (loc, TypeClassError + (env, UnsatisfiableConstraints (evd, Some (evi, kind))))) let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m)) |