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/rewrite.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/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 9e017bbd8f..171d77dd28 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -916,7 +916,7 @@ let apply_strategy (s : strategy) env sigma concl cstr evars = let split_evars_once sigma evd = Evd.fold_undefined (fun ev evi deps -> if Intset.mem ev deps then - Intset.union (Class_tactics.evars_of_evi evi evd) deps + Intset.union (Evarutil.undefined_evars_of_evar_info evd evi) deps else deps) evd sigma let existentials_of_evd evd = |