diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-03 20:22:33 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-03 20:22:33 +0000 |
| commit | c97a507293db3d4627250ecc433d71f48b0df130 (patch) | |
| tree | 11f39ffdeb879f2a36f69aeee31e9651bf6c94d3 /plugins/dp | |
| 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 'plugins/dp')
0 files changed, 0 insertions, 0 deletions