diff options
| author | letouzey | 2008-11-14 17:16:44 +0000 |
|---|---|---|
| committer | letouzey | 2008-11-14 17:16:44 +0000 |
| commit | 76c005d5d27e140cb9f0b70ed6390e5f291b3b37 (patch) | |
| tree | a786db593b85553b35b186d314e7a325285d5f41 /dev/include | |
| parent | b56e2c54f8a0e79f13ab16bd089e39033e3da75b (diff) | |
Faster comparison of universes
- compare the integer indexes first, in order to avoid
comparing the dirpath part if possible
- use an ad-hoc comparison function rather than Pervasives.compare
(slightly faster during my tests on the compcert contrib)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11589 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions