diff options
| author | letouzey | 2011-02-03 20:22:33 +0000 |
|---|---|---|
| committer | letouzey | 2011-02-03 20:22:33 +0000 |
| commit | c97a507293db3d4627250ecc433d71f48b0df130 (patch) | |
| tree | 11f39ffdeb879f2a36f69aeee31e9651bf6c94d3 /tactics/class_tactics.ml4 | |
| parent | 177fd2107c451c477ac839af339c698e10b9df18 (diff) | |
Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)
After r13717, we concentrate on undefined evars. But doing so
too naively was breaking Class_tactics.split_evars, since defined
evars may point to undefined ones. We should not ignore them,
but rather traverse them, which is now done by functions
Evarutil.undefined_evars_of_*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13809 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/class_tactics.ml4')
| -rw-r--r-- | tactics/class_tactics.ml4 | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 4b1500ea91..6300c699ba 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -469,24 +469,18 @@ let rec merge_deps deps = function merge_deps (Intset.union deps hd) tl else hd :: merge_deps deps tl -let evars_of_evi evi evm = - Intset.filter (is_undefined evm) - (Intset.union - (Evarutil.evars_of_term evi.evar_concl) - (Evarutil.evars_of_named_context (evar_filtered_context evi))) - let deps_of_constraints cstrs deps evm = List.fold_right (fun (_, _, x, y) deps -> - let evs = - Intset.filter (is_defined evm) - (Intset.union (Evarutil.evars_of_term x) (Evarutil.evars_of_term y)) - in merge_deps evs deps) + let evx = Evarutil.undefined_evars_of_term evm x + and evy = Evarutil.undefined_evars_of_term evm y + in merge_deps (Intset.union evx evy) deps) cstrs deps let evar_dependencies evm = Evd.fold_undefined (fun ev evi acc -> - merge_deps (Intset.add ev (evars_of_evi evi evm)) acc) + merge_deps + (Intset.add ev (Evarutil.undefined_evars_of_evar_info evm evi)) acc) evm [] (** [split_evars] returns groups of undefined evars according to dependencies *) |