Misc improvements about evar_map

 - A Evd.defined_evars to keep only this part of the evar_map
 - One Evd.fold less in Typeclasses.mark_unresolvables
 - We check that only undefined evar_map could be set unresolvable
 - A duplicated function in himsg.ml

TODO: some calls to Evd.fold(_undefined) would be faster if written
as Map.map or Map.mapi.

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

7 files changed, 24 insertions, 21 deletions

diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 420e25149f..3b95784ddd 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -150,6 +150,7 @@ val tj_nf_evar :
 
 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
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c70c13d9ec..3b96a4a3ba 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -110,6 +110,7 @@ module EvarInfoMap = struct
     ExistentialMap.fold (fun evk evi l -> (evk,evi)::l) undef []
 
   let undefined_evars (def,undef) = (ExistentialMap.empty,undef)
+  let defined_evars (def,undef) = (def,ExistentialMap.empty)
 
   let find (def,undef) k =
     try ExistentialMap.find k def
@@ -350,6 +351,7 @@ module EvarMap = struct
   let to_list (sigma,_) = EvarInfoMap.to_list sigma
   let undefined_list (sigma,_) = EvarInfoMap.undefined_list sigma
   let undefined_evars (sigma,sm) = (EvarInfoMap.undefined_evars sigma, sm)
+  let defined_evars (sigma,sm) = (EvarInfoMap.defined_evars sigma, sm)
   let fold (sigma,_) = EvarInfoMap.fold sigma
   let fold_undefined (sigma,_) = EvarInfoMap.fold_undefined sigma
   let define (sigma,sm) k v = (EvarInfoMap.define sigma k v, sm)
@@ -485,6 +487,7 @@ let mem d e = EvarMap.mem d.evars e
 let to_list d = EvarMap.to_list d.evars
 let undefined_list d = EvarMap.undefined_list d.evars
 let undefined_evars d = { d with evars=EvarMap.undefined_evars d.evars }
+let defined_evars d = { d with evars=EvarMap.defined_evars d.evars }
 (* spiwack: not clear what folding over an evar_map, for now we shall
     simply fold over the inner evar_map. *)
 let fold f d a = EvarMap.fold d.evars f a
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 90da5d389c..751009434e 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -182,6 +182,7 @@ val evars_reset_evd  : evar_map ->  evar_map -> evar_map
                    for moving to evarutils *)
 val is_undefined_evar :  evar_map -> constr -> bool
 val undefined_evars : evar_map -> evar_map
+val defined_evars : evar_map -> evar_map
 (* [fold_undefined f m] iterates ("folds") function [f] over the undefined
     evars (that is, whose value is [Evar_empty]) of map [m].
     It optimizes the call of {!Evd.fold} to [f] and [undefined_evars m] *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index bb25d06636..84815e0988 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -339,22 +339,30 @@ let is_implicit_arg k =
    This is essentially a hack to mark which evars correspond to
    goals and do not need to be resolved when we have nested [resolve_all_evars]
    calls (e.g. when doing apply in an External hint in typeclass_instances).
-   Would be solved by having real evars-as-goals. *)
+   Would be solved by having real evars-as-goals.
+
+   Nota: we will only check the resolvability status of undefined evars.
+ *)
 
 let resolvable = Store.field ()
 open Store.Field
 
 let is_resolvable evi =
+  assert (evi.evar_body = Evar_empty);
   Option.default true (resolvable.get evi.evar_extra)
 
-let mark_unresolvable evi =
+let mark_unresolvable_undef evi =
   let t = resolvable.set false evi.evar_extra in
   { evi with evar_extra = t }
 
+let mark_unresolvable evi =
+  assert (evi.evar_body = Evar_empty);
+  mark_unresolvable_undef evi
+
 let mark_unresolvables sigma =
-  Evd.fold (fun ev evi evs ->
-    Evd.add evs ev (mark_unresolvable evi))
-    sigma Evd.empty
+  Evd.fold_undefined (fun ev evi evs ->
+    Evd.add evs ev (mark_unresolvable_undef evi))
+    sigma (Evd.defined_evars sigma)
 
 let has_typeclasses evd =
   Evd.fold_undefined (fun ev evi has -> has ||
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 871da55116..800deefda4 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -74,6 +74,9 @@ val is_implicit_arg : hole_kind -> bool
 
 val instance_constructor : typeclass -> constr list -> constr * types
 
+(** Resolvability.
+    Only undefined evars could be marked or checked for resolvability. *)
+
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
 val mark_unresolvables : evar_map -> evar_map
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index bc415e78ac..2f85668a77 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -54,17 +54,9 @@ let evars_to_goals p evm =
 	let evi', goal = p evm ev evi in
 	let gls' = if goal then (ev,Goal.V82.build ev) :: gls else gls in
 	(gls', Evd.add evm' ev evi'))
-      evm ([], Evd.empty)
+      evm ([], Evd.defined_evars evm)
   in
-  if goals = [] then None
-  else
-    let goals = List.rev goals in
-    (** old defined evars of [evm] + new undefined ones of [evm'] *)
-    let evm' =
-      Evd.fold_undefined (fun ev evi evm -> Evd.add evm ev evi) evm' evm
-    in
-    let evm' = evars_reset_evd evm' evm in
-    Some (goals, evm')
+  if goals = [] then None else Some (List.rev goals, evm')
 
 (** Typeclasses instance search tactic / eauto *)
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 01eca8cb21..d14b8cccce 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -547,13 +547,8 @@ let explain_no_instance env (_,id) l =
   str "applied to arguments" ++ spc () ++
     prlist_with_sep pr_spc (pr_lconstr_env env) l
 
-let undefined_evars evm =
-  Evd.fold_undefined (fun ev evi undef ->
-      Evd.add undef ev (Evarutil.nf_evar_info evm evi)
-  ) evm Evd.empty
-
 let pr_constraints printenv env evm =
-  let evm = undefined_evars evm in
+  let evm = Evarutil.nf_evars_undefined evm in
   let l = Evd.to_list evm in
   let (ev, evi) = List.hd l in
     if List.for_all (fun (ev', evi') ->