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

1 files changed, 16 insertions, 2 deletions

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 787e43c15..dc9b624fb 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -507,16 +507,30 @@ let explain_no_instance env (_,id) l =
   str "applied to arguments" ++ spc () ++ 
     prlist_with_sep pr_spc (pr_lconstr_env env) l
 
+let pr_constraints env evm =
+  let l = Evd.to_list evm in
+  let (ev, evi) = List.hd l in
+    if List.for_all (fun (ev', evi') ->
+      eq_named_context_val evi.evar_hyps evi'.evar_hyps) l
+    then
+      let pe = pr_ne_context_of (str "In environment:") (mt ()) 
+	(reset_with_named_context evi.evar_hyps env) in
+	pe ++ fnl () ++ 
+	  prlist_with_sep (fun () -> fnl ()) 
+	  (fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l
+    else
+      pr_evar_map evm
+      
 let explain_unsatisfiable_constraints env evd constr =
   let evm = Evd.evars_of evd in
   match constr with
   | None ->
       str"Unable to satisfy the following typeclass constraints:" ++ fnl() ++
-	Evd.pr_evar_map evm
+	pr_constraints env evm
   | Some (evi, k) -> 
       explain_unsolvable_implicit env evi k None ++ fnl () ++
 	if List.length (Evd.to_list evm) > 1 then
-	  str"With the following typeclass constraints:" ++ 
+	  str"With the following meta variables:" ++ 
 	    fnl() ++ Evd.pr_evar_map evm 
 	else mt ()