diff options
author | 2017-03-24 15:50:21 +0100 | |
---|---|---|
committer | 2017-04-27 15:15:42 +0200 | |
commit | 051f2c1be929a46a0713b47b072bb5be0a7558d0 (patch) | |
tree | 9071a28a89d83bb6cffb82d0a3a3716b10a00e4f /kernel/vars.mli | |
parent | bc6de5aa4e00dfc19c4866de4876f6213546fa5c (diff) |
Fast path when checking equality of universe levels in UState.
We export the relevant level equality function in UGraph which is way faster
than checking that each one is smaller than the other as universes.
Diffstat (limited to 'kernel/vars.mli')
0 files changed, 0 insertions, 0 deletions