diff options
| author | letouzey | 2011-03-03 17:33:00 +0000 |
|---|---|---|
| committer | letouzey | 2011-03-03 17:33:00 +0000 |
| commit | 28a4f96caa3de3b43c3dc54eea4c221bee56b282 (patch) | |
| tree | 2a65e82eb35169fad22f41ec29f44271fcc48582 /plugins/xml | |
| parent | ac789d8826023e4b63bd459da2e4748fc68ad9e0 (diff) | |
Propagate recent kernel changes to the checker
Cf in particular commits 13807 (about inlining) and 13835-13836
(changing the internal structure of delta_resolver and substitution).
A pity we should duplicate so much code in the Checker...
I tried to fix the corresponding val_* functions that check the
integrity of the .vo, it seems to work, but I'm not familiar with this code.
After this commit, apparently "make validate" accepts all the stdlib again,
apart the new file setoid_ring/Ring2.v recently added by Loic,
where it says "type error" on ring_syntax1. To be investigated...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13865 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml')
0 files changed, 0 insertions, 0 deletions
