Improved the efficiency of evars traverals thanks to a split of

evar_map into a map for defined evars and a map for undefined evars.
Even before Spiwack's new proof engine, some Evd.fold were very
costly, e.g. in check_evars or progress_evar_map. With the new proof
engine, undefined evars traversals are apparently even more common (at
least, it improves significantly the complexity of some calls to omega
in JordanCurveTheorem - a new factor 5-7 after the factor 5-6 obtained
by removal of evar_merge in clenv_fchain in commit 13007, arriving to
figures comparable to the 8.3 ones).

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

13 files changed, 158 insertions, 134 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index c240d5f530..43d54da23a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,13 @@
 = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
 =========================================
 
+** Optimizing calls to Evd functions **
+
+Evars are split into defined evars and undefined evars; for
+efficiency, when an evar is known to be undefined, it is preferable to
+use specific functions about undefined evars since these ones are
+generally fewer than the defined ones.
+
 ** Internal tactics renamed
 
 There is no more difference between bindings and ebindings. The
diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis
index d23bf835b4..4c27d808b9 100644
--- a/dev/doc/perf-analysis
+++ b/dev/doc/perf-analysis
@@ -7,7 +7,7 @@ Dec 1, 2009 - Dec 19, 2009: Temporary addition of [forall x, P x] hints to
 
 Oct 19, 2009: Change in modules (CoLoR +35%)
 
-Aug 9, 2009: new files added in AreaMethod 
+Aug 9, 2009: new files added in AreaMethod
 
 May 21, 2008: New version of CoRN
   (needs +84% more time to compile)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4b76b77095..ad4e700897 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -514,7 +514,7 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
 	solve_simple_eqn ~choose:true evar_conv_x env i (None,ev1,t2))]
 
 let choose_less_dependent_instance evk evd term args =
-  let evi = Evd.find evd evk in
+  let evi = Evd.find_undefined evd evk in
   let subst = make_pure_subst evi args in
   let subst' = List.filter (fun (id,c) -> c = term) subst in
   if subst' = [] then error "Too complex unification problem." else
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index fbfb33cc37..000c062832 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -28,10 +28,10 @@ exception Uninstantiated_evar of existential_key
 
 let rec whd_ise sigma c =
   match kind_of_term c with
-    | Evar (evk,args as ev) when Evd.mem sigma evk ->
-	if Evd.is_defined sigma evk then
-          whd_ise sigma (existential_value sigma ev)
-	else raise (Uninstantiated_evar evk)
+  | Evar (evk,_ as ev) when Evd.is_defined sigma evk ->
+      whd_ise sigma (existential_value sigma ev)
+  | Evar (evk,_) when Evd.is_undefined sigma evk ->
+      raise (Uninstantiated_evar evk)
   | _ -> c
 
 
@@ -39,7 +39,7 @@ let rec whd_ise sigma c =
 let whd_castappevar_stack sigma c =
   let rec whrec (c, l as s) =
     match kind_of_term c with
-      | Evar (evk,args as ev) when Evd.mem sigma evk & Evd.is_defined sigma evk
+      | Evar (evk,args as ev) when Evd.is_defined sigma evk
 	  -> whrec (existential_value sigma ev, l)
       | Cast (c,_,_) -> whrec (c, l)
       | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
@@ -100,7 +100,7 @@ let collect_evars emap c =
   let rec collrec acc c =
     match kind_of_term c with
       | Evar (evk,_) ->
-	  if Evd.mem emap evk & not (Evd.is_defined emap evk) then evk::acc
+	  if Evd.is_undefined emap evk then evk::acc
 	  else (* No recursion on the evar instantiation *) acc
       | _         ->
 	  fold_constr collrec acc c in
@@ -145,14 +145,11 @@ let evars_to_metas sigma (emap, c) =
       | _ -> map_constr replace c in
   (sigma', replace c)
 
-(* The list of non-instantiated existential declarations *)
+(* The list of non-instantiated existential declarations (order is important) *)
 
 let non_instantiated sigma =
-  List.rev begin
-    Evd.fold_undefined begin fun ev evi l ->
-      (ev,nf_evar_info sigma evi)::l
-    end sigma []
-  end
+  let listev = Evd.undefined_list sigma in
+  List.map (fun (ev,evi) -> (ev,nf_evar_info sigma evi)) listev
 
 (**********************)
 (* Creating new evars *)
@@ -423,7 +420,7 @@ let extend_evar env evdref k (evk1,args1) c =
     let n = Array.length v - Array.length v2 in
     for i = 0 to Array.length v2 - 1 do v.(n+i) <- v2.(i) done;
     v in
-  let evi1 = Evd.find !evdref evk1 in
+  let evi1 = Evd.find_undefined !evdref evk1 in
   let named_sign',rel_sign',ty =
     if k = 0 then [], [], ty
     else shrink_context env (List.rev (make_pure_subst evi1 args1)) ty in
@@ -496,7 +493,7 @@ let rec check_and_clear_in_constr evdref err ids c =
             List.iter check vars; c
 
       | Evar (evk,l as ev) ->
-	  if Evd.is_defined_evar !evdref ev then
+	  if Evd.is_defined !evdref evk then
 	    (* If evk is already defined we replace it by its definition *)
 	    let nc = whd_evar !evdref c in
 	      (check_and_clear_in_constr evdref err ids nc)
@@ -506,7 +503,7 @@ let rec check_and_clear_in_constr evdref err ids c =
 	       arguments. Concurrently, we build a new evar
 	       corresponding to e where hypotheses of ids have been
 	       removed *)
-	    let evi = Evd.find !evdref evk in
+	    let evi = Evd.find_undefined !evdref evk in
 	    let ctxt = Evd.evar_filtered_context evi in
 	    let (nhyps,nargs,rids) =
 	      List.fold_right2
@@ -1219,7 +1216,7 @@ let status_changed lev (pbty,_,t1,t2) =
 
 let solve_refl conv_algo env evd evk argsv1 argsv2 =
   if argsv1 = argsv2 then evd else
-  let evi = Evd.find evd evk in
+  let evi = Evd.find_undefined evd evk in
   (* Filter and restrict if needed *)
   let evd,evk,args =
     restrict_upon_filter evd evi evk
@@ -1334,19 +1331,37 @@ let check_evars env initial_sigma evd c =
 	      (match k with
 	      | ImplicitArg (gr, (i, id), false) -> ()
 	      | _ ->
-		  let evi = nf_evar_info sigma (Evd.find sigma evk) in
+		  let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in
 		    error_unsolvable_implicit loc env sigma evi k None)
       | _ -> iter_constr proc_rec c
   in proc_rec c
 
-(* This returns the evars of [sigma] that are not in [sigma0] and
-   [sigma] minus these evars *)
-
-let subtract_evars sigma0 sigma =
-  Evd.fold (fun evk ev (sigma,sigma' as acc) ->
-    if Evd.mem sigma0 evk || Evd.mem sigma' evk then acc else
-      (Evd.remove sigma evk,Evd.add sigma' evk ev))
-    sigma (sigma,Evd.empty)
+(* Substitutes undefined evars by evars of same context up to renaming *)
+
+let subst_evar_evar subst c =
+  let rec aux c = match kind_of_term c with
+  | Evar (evk,args) ->
+      let evk' = try ExistentialMap.find evk subst with Not_found -> evk in
+      mkEvar (evk',Array.map aux args)
+  | _ -> map_constr aux c
+  in aux c
+
+let subst_undefined_evar_info_evar subst evi =
+  { evi with
+    evar_hyps = map_named_val (subst_evar_evar subst) evi.evar_hyps;
+    evar_concl = subst_evar_evar subst evi.evar_concl }
+
+open Rawterm
+
+let subst_evar_evar_in_constr_with_bindings subst (c,bl) =
+  (subst_evar_evar subst c,
+   match bl with
+   | ImplicitBindings largs ->
+       ImplicitBindings (List.map (subst_evar_evar subst) largs)
+   | ExplicitBindings lbind ->
+       ExplicitBindings (List.map (on_pi3 (subst_evar_evar subst)) lbind)
+   | NoBindings ->
+       NoBindings)
 
 (* Operations on value/type constraints *)
 
@@ -1393,7 +1408,7 @@ let mk_valcon c = Some c
    cumulativity now includes Prop and Set in Type...
    It is, but that's not too bad *)
 let define_evar_as_abstraction abs evd (ev,args) =
-  let evi = Evd.find evd ev in
+  let evi = Evd.find_undefined evd ev in
   let evenv = evar_unfiltered_env evi in
   let (evd1,dom) = new_evar evd evenv (new_Type()) ~filter:(evar_filter evi) in
   let nvar =
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index de50a87610..cbdc20f92a 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -87,7 +87,6 @@ val solve_simple_eqn :
    new unresolved evar remains in [c] *)
 val check_evars : env -> evar_map -> evar_map -> constr -> unit
 
-val subtract_evars : evar_map -> evar_map -> evar_map * evar_map 
 val define_evar_as_product : evar_map -> existential -> evar_map * types
 val define_evar_as_lambda : evar_map -> existential -> evar_map * types
 val define_evar_as_sort : evar_map -> existential -> evar_map * sorts
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 61a0353dd9..ed18f5e974 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -79,10 +79,10 @@ let eq_evar_info ei1 ei2 =
     ei1.evar_body = ei2.evar_body
 
 (* spiwack: Revised hierarchy :
-      - ExistentialMap ( Maps of existential_keys )
-      - EvarInfoMap ( .t = evar_info ExistentialMap.t )
-      - EvarMap ( .t = EvarInfoMap.t * sort_constraints )
-      - evar_map (exported)
+   - ExistentialMap ( Maps of existential_keys )
+   - EvarInfoMap ( .t = evar_info ExistentialMap.t * evar_info ExistentialMap )
+   - EvarMap ( .t = EvarInfoMap.t * sort_constraints )
+   - evar_map (exported)
 *)
 
 module ExistentialMap = Intmap
@@ -93,47 +93,70 @@ exception NotInstantiatedEvar
 
 
 module EvarInfoMap = struct
-  type t = evar_info ExistentialMap.t 
+  type t = evar_info ExistentialMap.t * evar_info ExistentialMap.t
 
-  let empty = ExistentialMap.empty 
-  let is_empty  = ExistentialMap.is_empty 
+  let empty = ExistentialMap.empty, ExistentialMap.empty
+  let is_empty (def,undef) =
+    (ExistentialMap.is_empty def, ExistentialMap.is_empty undef)
 
-  let to_list evc = (* Workaround for change in Map.fold behavior *)
-    (* spiwack: seems to arrange the items in decreasing order.
-        Which would also be the behaviour of a naive [fold].
-        I don't understand above comment. *)
+  let to_list (def,undef) =
+    (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
     let l = ref [] in
-    ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) evc;
+    ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) def;
+    ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) undef;
     !l
 
-  let dom evc = ExistentialMap.fold (fun evk _ acc -> evk::acc) evc []
-  let find evc k = ExistentialMap.find k evc
-  let remove evc k = ExistentialMap.remove k evc 
-  let mem evc k = ExistentialMap.mem k evc
-  let fold = ExistentialMap.fold
-  let exists evc f = ExistentialMap.fold (fun k v b -> b || f k v) evc false
+  let undefined_list (def,undef) =
+    (* Order is important: needs ocaml >= 3.08.4 from which "fold" is a
+       "fold_left" *)
+    ExistentialMap.fold (fun evk evi l -> (evk,evi)::l) undef []
+
+  let undefined_evars (def,undef) = (ExistentialMap.empty,undef)
+
+  let find (def,undef) k =
+    try ExistentialMap.find k def
+    with Not_found -> ExistentialMap.find k undef
+  let find_undefined (def,undef) k = ExistentialMap.find k undef
+  let remove (def,undef) k =
+    (ExistentialMap.remove k def,ExistentialMap.remove k undef)
+  let mem (def,undef) k =
+    ExistentialMap.mem k def || ExistentialMap.mem k undef
+  let fold (def,undef) f a =
+    ExistentialMap.fold f def (ExistentialMap.fold f undef a)
+  let fold_undefined (def,undef) f a =
+    ExistentialMap.fold f undef a
+  let exists_undefined (def,undef) f =
+    ExistentialMap.fold (fun k v b -> b || f k v) undef false
+
+  let add (def,undef) evk newinfo =
+    if newinfo.evar_body = Evar_empty then
+      (def,ExistentialMap.add evk newinfo undef)
+    else
+      (ExistentialMap.add evk newinfo def,undef)
 
-  let add evd evk newinfo =  ExistentialMap.add evk newinfo evd
+  let add_undefined (def,undef) evk newinfo =
+    assert (newinfo.evar_body = Evar_empty);
+    (def,ExistentialMap.add evk newinfo undef)
 
-  let map = ExistentialMap.map
+  let map f (def,undef) = (ExistentialMap.map f def, ExistentialMap.map f undef)
 
-  let define evd evk body =
+  let define (def,undef) evk body =
     let oldinfo =
-      try find evd evk
-      with Not_found -> error "Evd.define: cannot define undeclared evar" in
+      try ExistentialMap.find evk undef
+      with Not_found -> anomaly "Evd.define: cannot define undeclared evar" in
     let newinfo =
       { oldinfo with
 	  evar_body = Evar_defined body } in
       match oldinfo.evar_body with
-	| Evar_empty -> ExistentialMap.add evk newinfo evd
-	| _ -> anomaly "Evd.define: cannot define an evar twice"
-
-  let is_evar sigma evk = mem sigma evk
+	| Evar_empty ->
+	    (ExistentialMap.add evk newinfo def,ExistentialMap.remove evk undef)
+	| _ ->
+	    anomaly "Evd.define: cannot define an evar twice"
 
-  let is_defined sigma evk =
-    let info = find sigma evk in
-      not (info.evar_body = Evar_empty)
+  let is_evar = mem
 
+  let is_defined (def,undef) evk = ExistentialMap.mem evk def
+  let is_undefined (def,undef) evk = ExistentialMap.mem evk undef
 
   (*******************************************************************)
   (* Formerly Instantiate module *)
@@ -185,14 +208,6 @@ module EvarInfoMap = struct
     try Some (existential_value sigma ev)
     with NotInstantiatedEvar -> None
 
-  (* Combinators on undefined evars. *)
-  let fold_undefined f  = ExistentialMap.fold begin fun ev evi acc -> 
-                                          match evar_body evi with
-					  | Evar_empty -> f ev evi acc
-					  | _ -> acc
-                                       end
-
-  let undefined evm = fold_undefined ExistentialMap.add evm empty
 end
 
 (*******************************************************************)
@@ -329,41 +344,30 @@ module EvarMap = struct
   type t = EvarInfoMap.t * sort_constraints
   let empty = EvarInfoMap.empty, UniverseMap.empty
   let add (sigma,sm) k v = (EvarInfoMap.add sigma k v, sm)
-  let dom (sigma,_) = EvarInfoMap.dom sigma
+  let add_undefined (sigma,sm) k v = (EvarInfoMap.add_undefined sigma k v, sm)
   let find (sigma,_) = EvarInfoMap.find sigma
+  let find_undefined (sigma,_) = EvarInfoMap.find_undefined sigma
   let remove (sigma,sm) k = (EvarInfoMap.remove sigma k, sm)
   let mem (sigma,_) = EvarInfoMap.mem sigma
   let to_list (sigma,_) = EvarInfoMap.to_list sigma
-  let fold f (sigma,_) = EvarInfoMap.fold f sigma
+  let undefined_list (sigma,_) = EvarInfoMap.undefined_list sigma
+  let undefined_evars (sigma,sm) = (EvarInfoMap.undefined_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)
   let is_evar (sigma,_) = EvarInfoMap.is_evar sigma
   let is_defined (sigma,_) = EvarInfoMap.is_defined sigma
+  let is_undefined (sigma,_) = EvarInfoMap.is_undefined sigma
   let existential_value (sigma,_) = EvarInfoMap.existential_value sigma
   let existential_type (sigma,_) = EvarInfoMap.existential_type sigma
   let existential_opt_value (sigma,_) = EvarInfoMap.existential_opt_value sigma
   let progress_evar_map (sigma1,sm1 as x) (sigma2,sm2 as y) = not (x == y) &&
-    (EvarInfoMap.exists sigma1
-      (fun k v -> v.evar_body = Evar_empty &&
-        (EvarInfoMap.find sigma2 k).evar_body <> Evar_empty)
+    (EvarInfoMap.exists_undefined sigma1
+      (fun k v -> assert (v.evar_body = Evar_empty);
+        EvarInfoMap.is_defined sigma2 k)
     || not (UniverseMap.equal (=) sm1 sm2))
 
-  (* spiwack: used to workaround a bug in clenv: evar_merge
-        could merge an "old" version of an evar map into
-        a more up to date and erase evar definitions (in the case
-        of [constructor_tac] it actually erased a goal in some cases).
-       This is due to the fact that [open_constr] carry around their own
-       sigma which can be outdated by other operations. *)
-  let add_if_more_recent evd evk newinfo =
-    if newinfo.evar_body = Evar_empty && mem evd evk then
-	evd
-    else
-      add evd evk newinfo
-
-  let merge e e' = fold (fun n v sigma -> add_if_more_recent sigma n v) e' e
-
-  (* combinators on undefined values *)
-  let undefined (sigma,sm) = (EvarInfoMap.undefined sigma,sm)
-  let fold_undefined f (sigma,_) = EvarInfoMap.fold_undefined f sigma
+  let merge e e' = fold e' (fun n v sigma -> add sigma n v) e
 
 end
 
@@ -475,17 +479,21 @@ let merge d1 d2 = {
 }
 let add d e i = { d with evars=EvarMap.add d.evars e i }
 let remove d e = { d with evars=EvarMap.remove d.evars e }
-let dom d = EvarMap.dom d.evars
 let find d e = EvarMap.find d.evars e
+let find_undefined d e = EvarMap.find_undefined d.evars e
 let mem d e = EvarMap.mem d.evars e
 (* spiwack: this function loses information from the original evar_map
    it might be an idea not to export it. *)
 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 }
 (* 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 f d.evars a
+let fold f d a = EvarMap.fold d.evars f a
+let fold_undefined f d a = EvarMap.fold_undefined d.evars f a
 let is_evar d e = EvarMap.is_evar d.evars e
 let is_defined d e = EvarMap.is_defined d.evars e
+let is_undefined d e = EvarMap.is_undefined d.evars e
 
 let existential_value d e = EvarMap.existential_value d.evars e
 let existential_type d e = EvarMap.existential_type d.evars e
@@ -556,7 +564,7 @@ let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd =
       filter)
   in
   { evd with
-    evars = EvarMap.add evd.evars evk
+    evars = EvarMap.add_undefined evd.evars evk
       {evar_hyps = hyps;
        evar_concl = ty;
        evar_body = Evar_empty;
@@ -571,12 +579,6 @@ let is_undefined_evar evd c = match kind_of_term c with
   | Evar ev -> not (is_defined_evar evd ev)
   | _ -> false
 
-let undefined_evars evd =
-  let evars = EvarMap.undefined evd.evars in
-  { evd with evars = evars }
-
-let fold_undefined f evd = EvarMap.fold_undefined f evd.evars
-
 (* extracts conversion problems that satisfy predicate p *)
 (* Note: conv_pbs not satisying p are stored back in reverse order *)
 let extract_conv_pbs evd p =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 40323cdb81..87e703463f 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -147,20 +147,21 @@ val is_empty : evar_map -> bool
 
 val add : evar_map -> evar -> evar_info -> evar_map
 
-val dom : evar_map -> evar list
 val find : evar_map -> evar -> evar_info
+val find_undefined : evar_map -> evar -> evar_info
 val remove : evar_map -> evar -> evar_map
 val mem : evar_map -> evar -> bool
+val undefined_list : evar_map -> (evar * evar_info) list
 val to_list : evar_map -> (evar * evar_info) list
 val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
-
+val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 val merge : evar_map -> evar_map -> evar_map
-
 val define : evar -> constr -> evar_map -> evar_map
 
 val is_evar : evar_map -> evar -> bool
 
 val is_defined : evar_map -> evar -> bool
+val is_undefined : evar_map -> evar -> bool
 
 (** {6 ... } *)
 (** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
@@ -184,17 +185,12 @@ val is_undefined_evar :  evar_map -> constr -> bool
 val undefined_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].
-    Making it effectively equivalent to {!Evd.fold} applies to
-    [f] and [undefined_evars m] *)
-(* spiwack: at the moment, [fold_undefined] is defined rather naively.
-    But we can hope to enable some optimisation in the future, as
-    an evar_map contains typically few undefined evars compared to all
-    its evars. *)
+    It optimizes the call of {!Evd.fold} to [f] and [undefined_evars m] *)
 val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 val evar_declare :
   named_context_val -> evar -> types -> ?src:loc * hole_kind ->
       ?filter:bool list -> evar_map -> evar_map
-val evar_source : existential_key -> evar_map -> loc * hole_kind
+val evar_source : existential_key -> evar_map -> hole_kind located
 
 (* spiwack: this function seems to somewhat break the abstraction. 
    [evar_merge evd ev1] extends the evars of [evd] with [evd1] *)
@@ -205,6 +201,7 @@ type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * constr * constr
 val add_conv_pb :  evar_constraint -> evar_map -> evar_map
 
+module ExistentialMap : Map.S with type key = existential_key
 module ExistentialSet : Set.S with type elt = existential_key
 val extract_changed_conv_pbs : evar_map ->
       (ExistentialSet.t -> evar_constraint -> bool) ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2a716ee6ad..bfdc3fd8d6 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -370,7 +370,7 @@ let mark_unresolvables sigma =
 
 let has_typeclasses evd =
   Evd.fold_undefined (fun ev evi has -> has ||
-    (evi.evar_body = Evar_empty && is_class_evar evd evi && is_resolvable evi))
+    (is_class_evar evd evi && is_resolvable evi))
     evd false
 
 let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7ae05a85f0..b1b925f786 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -622,8 +622,8 @@ let w_merge env with_types flags (evd,metas,evars) =
 
     (* Process evars *)
     match evars with
-    | ((evn,_ as ev),rhs)::evars' ->
-    	if is_defined_evar evd ev then
+    | ((evk,_ as ev),rhs)::evars' ->
+	if Evd.is_defined evd evk then
 	  let v = Evd.existential_value evd ev in
 	  let (evd,metas',evars'') =
 	    unify_0 env evd topconv flags rhs v in
@@ -632,15 +632,17 @@ let w_merge env with_types flags (evd,metas,evars) =
           let rhs' = subst_meta_instances metas rhs in
           match kind_of_term rhs with
 	  | App (f,cl) when occur_meta rhs' ->
-	      if occur_evar evn rhs' then
-                error_occur_check env evd evn rhs';
+	      if occur_evar evk rhs' then
+                error_occur_check env evd evk rhs';
 	      if is_mimick_head f then
-		let evd' = mimick_evar evd flags f (Array.length cl) evn in
-		  w_merge_rec evd' metas evars eqns
+		let evd' =
+		  mimick_undefined_evar evd flags f (Array.length cl) evk in
+		w_merge_rec evd' metas evars eqns
 	      else
 		let evd', rhs'' = pose_all_metas_as_evars env evd rhs' in
-	  	  w_merge_rec (solve_simple_evar_eqn env evd' ev rhs'')
-		    metas evars' eqns
+		w_merge_rec (solve_simple_evar_eqn env evd' ev rhs'')
+		  metas evars' eqns
+
           | _ ->
 	      w_merge_rec (solve_simple_evar_eqn env evd ev rhs')
 		metas evars' eqns
@@ -682,8 +684,8 @@ let w_merge env with_types flags (evd,metas,evars) =
         w_merge_rec evd metas evars eqns
     | [] -> evd
 
-  and mimick_evar evd flags hdc nargs sp =
-    let ev = Evd.find evd sp in
+  and mimick_undefined_evar evd flags hdc nargs sp =
+    let ev = Evd.find_undefined evd sp in
     let sp_env = Global.env_of_context ev.evar_hyps in
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (evd'',mc,ec) =
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 35f7b4f023..faefc77a79 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -117,7 +117,7 @@ let return p =
   if not (is_done p) then
     raise UnfinishedProof
   else if has_unresolved_evar p then 
-    (* spiwack: for compatibility with <= 8.2 proof engine *)
+    (* spiwack: for compatibility with <= 8.3 proof engine *)
     raise HasUnresolvedEvar
   else
     Proofview.return p.state.proofview
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 1abd762538..d87d73d310 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -416,17 +416,19 @@ let tclINFO (tac : tactic) gls =
 
 (* Check that holes in arguments have been resolved *)
 
-let check_evars env sigma evm gl =
+let check_evars env sigma extsigma gl =
   let origsigma = gl.sigma in
   let rest =
-    Evd.fold (fun ev evi acc ->
-      if not (Evd.mem origsigma ev) && not (Evd.is_defined sigma ev)
-      then Evd.add acc ev evi else acc)
-      evm Evd.empty
+    Evd.fold_undefined (fun evk evi acc ->
+      if Evd.is_undefined extsigma evk & not (Evd.mem origsigma evk) then
+	evi::acc
+      else
+	acc)
+      sigma []
   in
-  if rest <> Evd.empty then
-    let (evk,evi) = List.hd (Evd.to_list rest) in
-    let (loc,k) = evar_source evk rest in
+  if rest <> [] then
+    let evi = List.hd rest in
+    let (loc,k) = evi.evar_source in
     let evi = Evarutil.nf_evar_info sigma evi in
     Pretype_errors.error_unsolvable_implicit loc env sigma evi k None
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index d5694ba899..d1b61caa63 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -71,7 +71,7 @@ type delayed_open_constr_with_bindings =
     env -> evar_map -> evar_map * constr with_bindings
 
 val general_multi_multi_rewrite :
-  evars_flag -> (bool * multi * delayed_open_constr_with_bindings) list -> 
+  evars_flag -> (bool * multi * delayed_open_constr_with_bindings) list ->
     clause -> (tactic * conditions) option -> tactic
 
 val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 90b3686f18..59d5cc3134 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1305,13 +1305,13 @@ let solve_remaining_evars fail_evar use_classes env initial_sigma evd c =
   let rec proc_rec c =
     let c = Reductionops.whd_evar !evdref c in
     match kind_of_term c with
-      | Evar (ev,args as k) when not (Evd.mem initial_sigma ev) ->
-            let (loc,src) = evar_source ev !evdref in
+      | Evar (evk,args as ev) when not (Evd.mem initial_sigma evk) ->
+            let (loc,src) = evar_source evk !evdref in
 	    let sigma =  !evdref in
-	    let evi = Evd.find sigma ev in
+	    let evi = Evd.find_undefined sigma evk in
 	    (try
-	      let c = solvable_by_tactic env evi k src in
-	      evdref := Evd.define ev c !evdref;
+	      let c = solvable_by_tactic env evi ev src in
+	      evdref := Evd.define evk c !evdref;
 	      c
 	    with Exit ->
               if fail_evar then