diff options
| author | letouzey | 2010-12-15 16:43:44 +0000 |
|---|---|---|
| committer | letouzey | 2010-12-15 16:43:44 +0000 |
| commit | 3c482becb02efe0a72e6363b6710094abdade86d (patch) | |
| tree | 4832f1c5dfc3697c9af2b79716f21b5b5cd49a8f /tactics/rewrite.ml4 | |
| parent | d536aeb0c465b62c708ba4c70fd31b82c24168a5 (diff) | |
Evar-related speed-up and clarifications in Class_tactics and Rewrite
Some functions are restricted to consider only undefined evars,
and some Evd.fold are replaced by Evd.fold_undefined. I'm less
sure about the modifications in rewrite.ml4, but in pratice
they seem to work well on the stdlib. I was planning to
say assert false for Not_found in Rewrite.evd_of_existentials
but some file of the stdlib doesn't like that (to be checked).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13717 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 860f162dbc..1faf9489b0 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -914,18 +914,20 @@ let apply_strategy (s : strategy) env sigma concl cstr evars = Some (Some (res.rew_prf, (res.rew_car, res.rew_from, res.rew_to))) let split_evars_once sigma evd = - Evd.fold (fun ev evi deps -> + Evd.fold_undefined (fun ev evi deps -> if Intset.mem ev deps then - Intset.union (Class_tactics.evars_of_evi evi) deps + Intset.union (Class_tactics.evars_of_evi evi evd) deps else deps) evd sigma let existentials_of_evd evd = - Evd.fold (fun ev evi acc -> Intset.add ev acc) evd Intset.empty + Evd.fold_undefined (fun ev _ acc -> Intset.add ev acc) evd Intset.empty let evd_of_existentials evd exs = - Intset.fold (fun i acc -> - let evi = Evd.find evd i in - Evd.add acc i evi) exs Evd.empty + Intset.fold + (fun ev acc -> + try Evd.add acc ev (Evd.find_undefined evd ev) + with Not_found -> acc) + exs Evd.empty let split_evars sigma evd = let rec aux deps = |