Speed-up refine by avoiding some calls to Evd.fold

 Instead of the full Evd.fold, Evd.fold_undefined seems enough in
 - Evarutil.push_dependent_evars
 - the nf_evars call in Evarutil.evars_to_metas
    (we hence create a function nf_evars_undefined and use it there)

 This should bring back Compcert into reasonable compilation time

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

1 files changed, 11 insertions, 4 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 4ad823e066..80fb4d94e9 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -59,8 +59,15 @@ let nf_evar_info evc info =
       | Evar_empty -> Evar_empty
       | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) }
 
-let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
-		     evm Evd.empty
+let nf_evars evm =
+  Evd.fold
+    (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
+    evm Evd.empty
+
+let nf_evars_undefined evm =
+  Evd.fold_undefined
+    (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
+    evm Evd.empty
 
 let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd
 
@@ -86,7 +93,7 @@ let collect_evars emap c =
   list_uniquize (collrec [] c)
 
 let push_dependent_evars sigma emap =
-  Evd.fold (fun ev {evar_concl = ccl} (sigma',emap') ->
+  Evd.fold_undefined (fun ev {evar_concl = ccl} (sigma',emap') ->
     List.fold_left
       (fun (sigma',emap') ev ->
 	(Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev))
@@ -111,7 +118,7 @@ let push_duplicated_evars sigma emap c =
 (* replaces a mapping of existentials into a mapping of metas.
    Problem if an evar appears in the type of another one (pops anomaly) *)
 let evars_to_metas sigma (emap, c) =
-  let emap = nf_evars emap in
+  let emap = nf_evars_undefined emap in
   let sigma',emap' = push_dependent_evars sigma emap in
   let sigma',emap' = push_duplicated_evars sigma' emap' c in
   let change_exist evar =