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

4 files changed, 20 insertions, 19 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