From bcb8c0d7f0f5552fe302d0071d28c6d3c58ba7ab Mon Sep 17 00:00:00 2001 From: ppedrot Date: Sat, 3 Nov 2012 00:55:50 +0000 Subject: [PATCH] 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 | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index d696db3e7818..c838b422dadf 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -118,14 +118,14 @@ 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 = @@ -133,15 +133,13 @@ module EvarInfoMap = struct 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)