Fix treatment of remaining unification constraints: raise a more

informative exception if some constraints do not unify. 
All calls except one used to raise a less informative exception when the
constraints weren't solved.


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

5 files changed, 18 insertions, 21 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 99e3c4e1d6..7cbaf124a7 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -128,7 +128,7 @@ let clenv_conv_leq env sigma t c bound =
   let evd = Evd.create_goal_evar_defs sigma in
   let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in
   let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in
-  let evars,_ = Evarconv.consider_remaining_unif_problems env evars in
+  let evars = Evarconv.consider_remaining_unif_problems env evars in
   let args = List.map (whd_evar evars) args in
   check_evars env sigma evars (applist (c,args));
   args
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 10f4db77aa..370904a686 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -553,10 +553,10 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 =
 let consider_remaining_unif_problems env evd =
   let (evd,pbs) = extract_all_conv_pbs evd in
   List.fold_left
-    (fun (evd,b as p) (pbty,env,t1,t2) ->
-      if b then apply_conversion_problem_heuristic env evd pbty t1 t2 else p)
-    (evd,true)
-    pbs
+    (fun evd (pbty,env,t1,t2) ->
+      let evd', b = apply_conversion_problem_heuristic env evd pbty t1 t2 in
+	if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2))
+    evd pbs
 
 (* Main entry points *)
 
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 9a4247bc26..28b960bb9f 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -34,7 +34,7 @@ val evar_eqappr_x :
       evar_map * bool
 (*i*)
 
-val consider_remaining_unif_problems : env -> evar_map -> evar_map * bool
+val consider_remaining_unif_problems : env -> evar_map -> evar_map
 
 val check_conv_record : constr * types list -> constr * types list ->
   constr * constr list * (constr list * constr list) *
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cfe028aa51..bed4d834d2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -674,15 +674,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
 	  (pretype tycon env evdref lvar c).uj_val
       | IsType ->
-	  (pretype_type empty_valcon env evdref lvar c).utj_val in
-    evdref := fst (consider_remaining_unif_problems env !evdref);
-    if resolve_classes then
+	  (pretype_type empty_valcon env evdref lvar c).utj_val 
+    in
+    if resolve_classes then (
+      evdref := consider_remaining_unif_problems env !evdref;
       evdref :=
         Typeclasses.resolve_typeclasses ~onlyargs:false
-	  ~split:true ~fail:fail_evar env !evdref;
+	  ~split:true ~fail:fail_evar env !evdref);
+    evdref := consider_remaining_unif_problems env !evdref;
     let c = if expand_evar then nf_evar !evdref c' else c' in
-    if fail_evar then check_evars env Evd.empty !evdref c;
-    c
+      if fail_evar then check_evars env Evd.empty !evdref c;
+      c
 
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
@@ -692,7 +694,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let understand_judgment sigma env c =
     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 = consider_remaining_unif_problems env !evdref in
     let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:false
       ~fail:true env evd
     in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 32b51eac49..438a584698 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -554,12 +554,9 @@ let pose_all_metas_as_evars env evd t =
 let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
   let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
-  let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in
-  if b then
-    let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
+  let evd' = Evarconv.consider_remaining_unif_problems env evd' in
+  let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
     (evd',j'.uj_val)
-  else
-    error "Cannot solve unification constraints"
 
 let w_coerce_to_type env evd c cty mvty =
   let evd,mvty = pose_all_metas_as_evars env evd mvty in
@@ -615,9 +612,7 @@ let order_metas metas =
 let solve_simple_evar_eqn env evd ev rhs =
   let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (None,ev,rhs) in
   if not b then error_cannot_unify env evd (mkEvar ev,rhs);
-  let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in
-  if not b then error "Cannot solve unification constraints";
-  evd
+  Evarconv.consider_remaining_unif_problems env evd
 
 (* [w_merge env sigma b metas evars] merges common instances in metas
    or in evars, possibly generating new unification problems; if [b]