diff options
| author | Pierre-Marie Pédrot | 2016-02-03 20:07:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-03 20:24:06 +0100 |
| commit | 5d9eaa378277ed96456fec5a2037a8da4f38c8e0 (patch) | |
| tree | ca8aca465c51893aef9f8237338ef4e4aca472e5 /kernel/nativecode.ml | |
| parent | 62c141be71dd3c542824c19429eac0fdd686c9cb (diff) | |
Optimizing the universes_of_constr_function.
Instead of relying on a costly set union, we take advantage of the fact
that instances are small compared to the set of universes.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions