diff options
| author | Pierre-Marie Pédrot | 2020-08-24 15:47:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-31 10:24:43 +0200 |
| commit | c3d8ab86e892ec85acc843be62f3de9060368b13 (patch) | |
| tree | 204859d49ef1c6dea0b2db4de26a708b50278ca6 /kernel/typeops.ml | |
| parent | 9c9bf136430213eacec8e32ad4909cf501141a48 (diff) | |
Use a faster algorithm to check for class existence.
There is a hidden invariant that guarantees that the class index and its
reference field are the same.
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions