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

10 files changed, 28 insertions, 31 deletions

diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index a2dd7d777..f51dd5409 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -453,7 +453,7 @@ let interp_recursive fixkind l boxed =
   let fixdefs = List.map out_def fixdefs in
 
   (* Instantiate evars and check all are resolved *)
-  let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in
+  let evd = Evarconv.consider_remaining_unif_problems env_rec !evdref in
   let evd = Typeclasses.resolve_typeclasses
     ~onlyargs:true ~split:true ~fail:false env_rec evd
   in
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 54f7aff1b..775397124 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -70,7 +70,7 @@ let merge_evms x y =
 let interp env isevars c tycon =
   let j = pretype tycon env isevars ([],[]) c in
   let _ = isevars := Evarutil.nf_evar_map !isevars in
-  let evd,_ = consider_remaining_unif_problems env !isevars in
+  let evd = consider_remaining_unif_problems env !isevars in
 (*   let unevd = undefined_evars evd in *)
   let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in
   let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:false env unevd' in
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index f909f9e0a..47882e771 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -576,11 +576,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  (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);
+    evdref := consider_remaining_unif_problems env !evdref;
     if resolve_classes then
-      evdref :=
-        Typeclasses.resolve_typeclasses ~onlyargs:false
+      (evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
 	  ~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
@@ -593,7 +593,7 @@ module SubtacPretyping_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 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/clenv.ml b/pretyping/clenv.ml
index 99e3c4e1d..7cbaf124a 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 10f4db77a..370904a68 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 9a4247bc2..28b960bb9 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 cfe028aa5..bed4d834d 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 32b51eac4..438a58469 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]
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 75f0daa7f..51c7e50a4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -256,9 +256,9 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
      () in
 
   (* Instantiate evars and check all are resolved *)
-  let evd,_ = consider_remaining_unif_problems env_params !evdref in
+  let evd = consider_remaining_unif_problems env_params !evdref in
   let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in
-  let sigma =  evd in
+  let sigma = evd in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
   let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
   let arities = List.map (nf_evar sigma) arities in
@@ -522,7 +522,7 @@ let interp_recursive isfix fixl notations =
       () in
 
   (* Instantiate evars and check all are resolved *)
-  let evd,_ = consider_remaining_unif_problems env_rec !evdref in
+  let evd = consider_remaining_unif_problems env_rec !evdref in
   let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in
   let fixtypes = List.map (nf_evar evd) fixtypes in
   let fixctxlength = List.map (fun (_,ctx) -> rel_context_nhyps ctx) fixctxs in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 0353261b9..c1c1a9671 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -68,7 +68,7 @@ let typecheck_params_and_fields id t ps nots fs =
   let env2,impls,newfs,data =
     interp_fields_evars evars env_ar nots (binders_of_decls fs)
   in
-  let evars,_ = Evarconv.consider_remaining_unif_problems env_ar !evars in
+  let evars = Evarconv.consider_remaining_unif_problems env_ar !evars in
   let evars = Typeclasses.resolve_typeclasses env_ar evars in
   let sigma =  evars in
   let newps = Evarutil.nf_rel_context_evar sigma newps in