diff options
| author | letouzey | 2010-12-13 17:42:58 +0000 |
|---|---|---|
| committer | letouzey | 2010-12-13 17:42:58 +0000 |
| commit | 1af6a60fc922d9b14bb619fd42743277e09a8816 (patch) | |
| tree | 485b1b3de65b5c6f502ed86fe63530598cbd75e4 | |
| parent | f94f726dd6783533535419ebf772ab672611f590 (diff) | |
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
| -rw-r--r-- | proofs/goal.ml | 22 |
1 files 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 |