diff options
| author | ppedrot | 2012-11-03 00:55:50 +0000 |
|---|---|---|
| committer | ppedrot | 2012-11-03 00:55:50 +0000 |
| commit | bcb8c0d7f0f5552fe302d0071d28c6d3c58ba7ab (patch) | |
| tree | 6f87a62791c50e93822418a135d649197a04230f | |
| parent | cf59f30fc9a4f5e90805b54a4c6d39c9bbd96e65 (diff) | |
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
| -rw-r--r-- | pretyping/evd.ml | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index d696db3e78..c838b422da 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) |