aboutsummaryrefslogtreecommitdiff
path: root/plugins/xml
diff options
context:
space:
mode:
authorletouzey2011-03-03 17:33:00 +0000
committerletouzey2011-03-03 17:33:00 +0000
commit28a4f96caa3de3b43c3dc54eea4c221bee56b282 (patch)
tree2a65e82eb35169fad22f41ec29f44271fcc48582 /plugins/xml
parentac789d8826023e4b63bd459da2e4748fc68ad9e0 (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