- Better error messages taking unif. constraints into account.

- Normalize evars in typeclasses eauto also before [intro].
- Disallow use of nf_evars variants that drop unif. constraints.

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

9 files changed, 24 insertions, 16 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 774180c67b..418f683319 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -70,6 +70,7 @@ let nf_evars_undefined evm =
     evm Evd.empty
 
 let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd
+let nf_evar_map_undefined evd = Evd.evars_reset_evd (nf_evars_undefined evd) evd
 
 (**********************)
 (* Creating new metas *)
@@ -118,7 +119,7 @@ let push_duplicated_evars sigma emap c =
 (* replaces a mapping of existentials into a mapping of metas.
    Problem if an evar appears in the type of another one (pops anomaly) *)
 let evars_to_metas sigma (emap, c) =
-  let emap = nf_evars_undefined emap in
+  let emap = nf_evar_map_undefined emap in
   let sigma',emap' = push_dependent_evars sigma emap in
   let sigma',emap' = push_duplicated_evars sigma' emap' c in
   let change_exist evar =
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index a4c07a0196..3127d87eda 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -154,15 +154,13 @@ val jv_nf_evar :
 val tj_nf_evar :
    evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
-val nf_evar_info : evar_map -> evar_info -> evar_info
-val nf_evars : evar_map -> evar_map
-val nf_evars_undefined : evar_map -> evar_map
-
 val nf_named_context_evar : evar_map -> named_context -> named_context
 val nf_rel_context_evar : evar_map -> rel_context -> rel_context
 val nf_env_evar : evar_map -> env -> env
 
+val nf_evar_info : evar_map -> evar_info -> evar_info
 val nf_evar_map : evar_map -> evar_map
+val nf_evar_map_undefined : evar_map -> evar_map
 
 (** Replacing all evars, possibly raising [Uninstantiated_evar] *)
 exception Uninstantiated_evar of existential_key
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 33ad751523..e5347b7f60 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -741,6 +741,10 @@ let pr_constraints pbs =
 	| Reduction.CUMUL -> "<=") ++
       spc() ++ print_constr t2) pbs)
 
+let pr_evar_map_constraints evd =
+  if evd.conv_pbs = [] then mt() 
+  else pr_constraints evd.conv_pbs++fnl()
+
 let pr_evar_map evd =
   let pp_evm =
     if evd.evars = EvarMap.empty then mt() else
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index e5a40b5a14..29c505d92f 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -276,6 +276,7 @@ type unsolvability_explanation = SeveralInstancesFound of int
    debug pretty-printer: *)
 
 val pr_evar_info : evar_info -> Pp.std_ppcmds
+val pr_evar_map_constraints : evar_map -> Pp.std_ppcmds
 val pr_evar_map : evar_map -> Pp.std_ppcmds
 val pr_metaset : Metaset.t -> Pp.std_ppcmds
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1ea2dbd002..e3b8dbc204 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -717,7 +717,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 = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:false
+    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true
       ~fail:true env !evdref
     in
     let evd = consider_remaining_unif_problems env evd in
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index cf7faed905..d17c783e9b 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -414,7 +414,7 @@ let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac =
 	| Some (evm', fk) -> Some (evars_reset_evd ~with_conv_pbs:true evm' evm, fk)
 	    
 let eauto_tac hints = 
-  fix (or_tac (then_tac normevars_tac (hints_tac hints)) intro_tac)
+  fix (then_tac normevars_tac (or_tac (hints_tac hints) intro_tac))
   
 let eauto ?(only_classes=true) ?st hints g =
   let gl = { it = make_autogoal ~only_classes ?st None g; sigma = project g } in
@@ -493,8 +493,9 @@ let split_evars evm =
 
 let evars_in_comp comp evm =
   try
-    Intset.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev))
-      comp Evd.empty
+    evars_reset_evd 
+      (Intset.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev))
+	 comp Evd.empty) evm
   with Not_found -> assert false
 
 let is_inference_forced p evd ev =
@@ -516,7 +517,7 @@ let is_mandatory p comp evd =
 (** In case of unsatisfiable constraints, build a nice error message *)
 
 let error_unresolvable env comp do_split evd =
-  let evd = Evarutil.nf_evars_undefined evd in
+  let evd = Evarutil.nf_evar_map_undefined evd in
   let evm = if do_split then evars_in_comp comp evd else evd in
   let _, ev = Evd.fold_undefined
     (fun ev evi (b,acc) ->
@@ -575,7 +576,8 @@ let resolve_all_evars debug m env p oevd do_split fail =
 	if fail && (not do_split || is_mandatory (p evd) comp evd)
 	then (* Unable to satisfy the constraints. *)
 	  error_unresolvable env comp do_split evd
-	else (* Best effort: do nothing *) oevd
+	else (* Best effort: do nothing on this component *) 
+	  docomp oevd comps
   in docomp oevd split
 
 let initial_select_evars onlyargs =
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 59e7fcca15..a14cf62870 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -182,7 +182,7 @@ module SearchProblem = struct
   let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl)
 
   let pr_goals gls =
-    let evars = Evarutil.nf_evars (Refiner.project gls) in
+    let evars = Evarutil.nf_evar_map (Refiner.project gls) in
       prlist (pr_ev evars) (sig_it gls)
 
   let filter_tactics glls l =
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 242a8e52b4..af1330a42b 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -255,7 +255,7 @@ let gen_sort_topo l evm =
 (* register real typeclass instance given a totally defined evd *)
 let declare_instance (k:global_reference -> rel_context -> constr list -> unit)
     (cl,gen,evm:signature) =
-  let evm = Evarutil.nf_evars evm in
+  let evm = Evarutil.nf_evar_map evm in
   let gen = gen_sort_topo gen evm in
   let (evm,gen) = List.fold_right
     (fun ev (evm,gen) ->
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 6af1f9d56c..60a3b89bb0 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -696,7 +696,7 @@ let explain_no_instance env (_,id) l =
     prlist_with_sep pr_spc (pr_lconstr_env env) l
 
 let pr_constraints printenv env evm =
-  let evm = Evarutil.nf_evars_undefined evm in
+  let evm = Evarutil.nf_evar_map_undefined evm in
   let l = Evd.to_list evm in
   let (ev, evi) = List.hd l in
     if List.for_all (fun (ev', evi') ->
@@ -706,12 +706,14 @@ let pr_constraints printenv env evm =
 	(reset_with_named_context evi.evar_hyps env) in
 	(if printenv then pe ++ fnl () else mt ()) ++
 	  prlist_with_sep (fun () -> fnl ())
-	  (fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l
+	  (fun (ev, evi) -> str(string_of_existential ev) ++ 
+	     str " : " ++ pr_lconstr evi.evar_concl) l ++ fnl() ++
+	  pr_evar_map_constraints evm
     else
       pr_evar_map evm
 
 let explain_unsatisfiable_constraints env evd constr =
-  let evm = Evarutil.nf_evars evd in
+  let evm = Evarutil.nf_evar_map evd in
   let undef = Evd.undefined_evars evm in
   match constr with
   | None ->