- 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

5 files changed, 10 insertions, 6 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 774180c67..418f68331 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 a4c07a019..3127d87ed 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 33ad75152..e5347b7f6 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 e5a40b5a1..29c505d92 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 1ea2dbd00..e3b8dbc20 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