From 1af6a60fc922d9b14bb619fd42743277e09a8816 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 13 Dec 2010 17:42:58 +0000
Subject: Goal: preventively replace an Evd.fold by an equivalent
 Evd.fold_undefined

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13710 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/goal.ml | 22 ++++++++--------------
 1 file changed, 8 insertions(+), 14 deletions(-)

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 8e0a678ac5..9f0d48bb1b 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -156,15 +156,11 @@ module Refinable = struct
 
 
   (* a pessimistic (i.e : there won't be many positive answers) filter
-     over evar_maps *)
-  let evar_map_filter f evm =
-    Evd.fold (fun ev evi r -> 
-		if f ev evi then 
-		  Evd.add r ev evi 
-		else 
-		  r
-	     ) 
-      evm 
+     over evar_maps, acting only on undefined evars *)
+  let evar_map_filter_undefined f evm =
+    Evd.fold_undefined
+      (fun ev evi r -> if f ev evi then Evd.add r ev evi else r)
+      evm
       Evd.empty
 
   (* Union, sorted in decreasing order, of two lists of evars in decreasing order. *)
@@ -201,11 +197,9 @@ module Refinable = struct
     (* [delta_evars] holds the evars that have been introduced by this
        refinement (but not immediatly solved) *)
     (* spiwack: this is the hackish part, don't know how to do any better though. *)
-    let delta_evars = evar_map_filter (fun ev evi ->
-					 evi.Evd.evar_body = Evd.Evar_empty &&
-                                         not (Evd.mem init_defs ev)
-				      )
-                                     post_defs
+    let delta_evars = evar_map_filter_undefined
+      (fun ev _ -> not (Evd.mem init_defs ev))
+      post_defs
     in
     (* [delta_evars] in the shape of a list of [evar]-s*)
     let delta_list = List.map fst (Evd.to_list delta_evars) in
-- 
cgit v1.2.3