From 90899bd52f32ef608754f937c5b23d250dc41ed8 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 17 Jun 2008 07:33:24 +0000
Subject: 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
---
 pretyping/typeclasses_errors.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping/typeclasses_errors.ml')

diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 72d23946cb..0907760189 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))
-- 
cgit v1.2.3