Fix typeclass error handling which was sometimes raising a Failure ("hd").

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15593 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 17 insertions, 16 deletions

diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 6575bbfe1f..3cd02f5444 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1222,9 +1222,9 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl =
     with
     | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
     | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
-	Refiner.tclFAIL_lazy 0
-	  (lazy (str"Unable to satisfy the rewriting constraints."
-		 ++ fnl () ++ Himsg.explain_typeclass_error env e))
+	Refiner.tclFAIL 0
+	  (str"Unable to satisfy the rewriting constraints."
+	   ++ fnl () ++ Himsg.explain_typeclass_error env e)
   in tac gl
 
 open Goal
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 0df2994b70..39554dd3d7 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -395,7 +395,7 @@ let explain_typeclass_resolution env evi k =
       fnl () ++ str "Could not find an instance for " ++
       pr_lconstr_env env evi.evar_concl ++
       pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env
-  | None -> mt()
+  | _ -> mt()
 
 let explain_unsolvable_implicit env evi k explain =
   str "Cannot infer " ++ explain_evar_kind env (Some evi) k ++
@@ -696,12 +696,8 @@ let explain_no_instance env (_,id) l =
 let is_goal_evar evi = match evi.evar_source with (_, Evar_kinds.GoalEvar) -> true | _ -> false
 
 let pr_constraints printenv env evm =
-  let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evm) in
-  let evm = fold_undefined 
-    (fun ev evi evm' -> 
-       if is_goal_evar evi then Evd.remove evm' ev else evm') evm evm
-  in
   let l = Evd.to_list evm in
+  assert(l <> []);
   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
@@ -717,18 +713,23 @@ let pr_constraints printenv env evm =
       pr_evar_map None evm
 
 let explain_unsatisfiable_constraints env evd constr =
-  let evm = Evarutil.nf_evar_map evd in
-  let undef = Evd.undefined_evars evm in
+  let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evd) in
+  (* Remove goal evars *)
+  let undef = fold_undefined 
+    (fun ev evi evm' -> 
+       if is_goal_evar evi then Evd.remove evm' ev else evm') evm evm
+  in
   match constr with
   | None ->
       str"Unable to satisfy the following constraints:" ++ fnl() ++
 	pr_constraints true env undef
   | Some (ev, k) ->
-      explain_unsolvable_implicit env (Evd.find evm ev) k None ++ fnl () ++
-	if List.length (Evd.to_list undef) > 1 then
-	  str"With the following constraints:" ++ fnl() ++
-	    pr_constraints false env (Evd.remove undef ev)
-	else mt ()
+      explain_typeclass_resolution env (Evd.find evm ev) k ++ fnl () ++
+	(let remaining = Evd.remove undef ev in
+	   if Evd.has_undefined remaining then
+	     str"With the following constraints:" ++ fnl() ++
+	       pr_constraints false env remaining
+	   else mt ())
 
 let explain_mismatched_contexts env c i j =
   str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++