Reversed roles of undefined/defined evars in Evd, thus saving precious

time when requesting only undefined evars (which is actually most often
the case, as in Goal.advance). Hopefully this should not disrupt anything.

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

pretyping/evd.ml

@@ -118,30 +118,28 @@ module EvarInfoMap = struct
   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
-    with Not_found -> ExistentialMap.find k undef
+  let find (def, undef) k =
+    try ExistentialMap.find k undef
+    with Not_found -> ExistentialMap.find k def
   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 mem (def, undef) k =
+    ExistentialMap.mem k undef || ExistentialMap.mem k def
   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 (def,undef) evk newinfo = match newinfo.evar_body with
+  | Evar_empty -> (def, ExistentialMap.add evk newinfo undef)
+  | _ -> (ExistentialMap.add evk newinfo def, undef)
 
-  let add_undefined (def,undef) evk newinfo =
-    assert (newinfo.evar_body = Evar_empty);
-    (def,ExistentialMap.add evk newinfo undef)
+  let add_undefined (def,undef) evk newinfo = match newinfo.evar_body with
+  | Evar_empty -> (def, ExistentialMap.add evk newinfo undef)
+  | _ -> assert false
 
   let map f (def,undef) = (ExistentialMap.map f def, ExistentialMap.map f undef)