Fix "unsatisfiable constraints" error messages to include all the

necessary information. Fix implementation of [split_evars] and 
use splitting more wisely as it has a big performance impact.


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

7 files changed, 35 insertions, 33 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bc0dba883..91cdff5fb 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -673,7 +673,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     if resolve_classes then
       evdref := 
         Typeclasses.resolve_typeclasses ~onlyargs:(not fail_evar)
-	  ~fail:fail_evar env !evdref;
+	  ~split:false ~fail:fail_evar env !evdref;
     let c = nf_evar !evdref c' in
     if fail_evar then check_evars env Evd.empty !evdref c;
     c
@@ -687,7 +687,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let evdref = ref (create_evar_defs sigma) in
     let j = pretype empty_tycon env evdref ([],[]) c in
     let evd,_ = consider_remaining_unif_problems env !evdref in
-    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env evd in
+    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:false
+      ~fail:true env evd 
+    in
     let j = j_nf_evar evd j in
     check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
     j
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index c7e3895e0..cec46d780 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -28,7 +28,7 @@ type typeclass_error =
     | NotAClass of constr
     | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
-    | UnsatisfiableConstraints of evar_defs * (evar_info * hole_kind) option
+    | UnsatisfiableConstraints of evar_defs * (existential_key * hole_kind) option
     | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
@@ -42,16 +42,14 @@ let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
 let no_instance env id args = typeclass_error env (NoInstance (id, args))
 
 let unsatisfiable_constraints env evd ev = 
-  let evd = Evd.undefined_evars evd in
-    match ev with
-    | None ->
-	raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
-    | Some ev ->
-	let evi = Evd.find evd ev in
-	let loc, kind = Evd.evar_source ev evd in
-	  raise (Stdpp.Exc_located (loc, TypeClassError
-	    (env, UnsatisfiableConstraints (evd, Some (evi, kind)))))
-	    
+  match ev with
+  | None ->
+      raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
+  | Some ev ->
+      let loc, kind = Evd.evar_source ev evd in
+	raise (Stdpp.Exc_located (loc, TypeClassError
+	  (env, UnsatisfiableConstraints (evd, Some (ev, kind)))))
+	  
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
 
 let rec unsatisfiable_exception exn =
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index b977a1a34..4af1333e9 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -25,11 +25,11 @@ open Libnames
 type contexts = Parameters | Properties
 
 type typeclass_error = 
-    | NotAClass of constr
-    | UnboundMethod of global_reference * identifier located (* Class name, method *)
-    | NoInstance of identifier located * constr list
-    | UnsatisfiableConstraints of evar_defs * (evar_info * hole_kind) option
-    | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
+  | NotAClass of constr
+  | UnboundMethod of global_reference * identifier located (* Class name, method *)
+  | NoInstance of identifier located * constr list
+  | UnsatisfiableConstraints of evar_defs * (existential_key * hole_kind) option
+  | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7f5bf4ece..c1bca3f9f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -701,7 +701,8 @@ let w_unify_core_0 env with_types cv_pb flags m n evd =
   in
   let evd = w_merge env with_types flags subst2 in
     if flags.resolve_evars then 
-      try Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:true env evd
+      try Typeclasses.resolve_typeclasses ~onlyargs:false ~split:false
+	~fail:true env evd
       with e when Typeclasses_errors.unsatisfiable_exception e ->
 	error_cannot_unify env evd (m, n)
     else evd
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 9146d02c5..1163547bf 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -417,9 +417,15 @@ let rec merge_deps deps = function
 	merge_deps (Intset.union deps hd) tl
       else hd :: merge_deps deps tl
 	
+let evars_of_evi evi =
+  Intset.union (Evarutil.evars_of_term evi.evar_concl) 
+    (match evi.evar_body with
+    | Evar_defined b -> Evarutil.evars_of_term b
+    | Evar_empty -> Intset.empty)
+
 let split_evars evm =
   Evd.fold (fun ev evi acc ->
-    let deps = Intset.union (Intset.singleton ev) (Evarutil.evars_of_term evi.evar_concl) in
+    let deps = Intset.union (Intset.singleton ev) (evars_of_evi evi) in
       merge_deps deps acc)
     evm []
 
@@ -430,7 +436,7 @@ let select_evars evs evm =
 
 let resolve_all_evars debug m env p oevd do_split fail =
   let oevm =  oevd in
-  let split = if do_split then split_evars (Evd.undefined_evars oevd) else [Intset.empty] in
+  let split = if do_split then split_evars oevd else [Intset.empty] in
   let p = if do_split then 
     fun comp ev evi -> (Intset.mem ev comp || not (Evd.mem oevm ev)) && p ev evi
     else fun _ -> p 
@@ -450,7 +456,7 @@ let resolve_all_evars debug m env p oevd do_split fail =
 	  match res with
 	  | None -> 
 	      if fail then 
-		(* Unable to satisfy the constraints. *)
+		(* Unable to satisfy the constraints. *)		
 		let evm = if do_split then select_evars comp evd else evd in
 		let _, ev = Evd.fold 
 		  (fun ev evi (b,acc) -> 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 7260f1fd7..32155f054 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -742,16 +742,10 @@ let apply_strategy (s : strategy) env sigma concl cstr evars =
 	evars := res.rew_evars;
 	Some (Some (res.rew_prf, (res.rew_car, res.rew_rel, res.rew_from, res.rew_to)))
 
-let evars_of_evi evi =
-  Intset.union (Evarutil.evars_of_term evi.evar_concl) 
-    (match evi.evar_body with
-    | Evar_defined b -> Evarutil.evars_of_term b
-    | Evar_empty -> Intset.empty)
-
 let split_evars_once sigma evd = 
   Evd.fold (fun ev evi deps ->
     if Intset.mem ev deps then 
-      Intset.union (evars_of_evi evi) deps
+      Intset.union (Class_tactics.evars_of_evi evi) deps
     else deps) evd sigma
     
 let existentials_of_evd evd =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e8a8dcb7c..b005aedf6 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -526,15 +526,16 @@ let pr_constraints printenv env evm =
       
 let explain_unsatisfiable_constraints env evd constr =
   let evm = Evarutil.nf_evars evd in
+  let undef = Evd.undefined_evars evm in
   match constr with
   | None ->
       str"Unable to satisfy the following constraints:" ++ fnl() ++
 	pr_constraints true env evm
-  | Some (evi, k) -> 
-      explain_unsolvable_implicit env evi k None ++ fnl () ++
-	if List.length (Evd.to_list evm) > 1 then
+  | 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 evm
+	    pr_constraints false env (Evd.remove undef ev)
 	else mt ()
 	
 let explain_mismatched_contexts env c i j =