diff options
| author | letouzey | 2011-02-11 16:53:52 +0000 |
|---|---|---|
| committer | letouzey | 2011-02-11 16:53:52 +0000 |
| commit | edbfb435e9d78db2bc1b6ae9d3808f808617d5e8 (patch) | |
| tree | bf881482f04e67656df5b4c26eb762f624cda67a /dev | |
| parent | 7d9d5157df272f6b276f3271cafd02d2488bae05 (diff) | |
Mod_subst: split delta_resolver in two tables (mp / kn)
This way, no more absurd mixing of mp/kn and Prefix_equiv/Equiv to
consider, and hence no more anomaly or assert false left in Mod_subst.
As we say here, "faut pas melanger les torchons et les serviettes" ...
With these two specialized tables, efficiency might also be better.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13835 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions