diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-03 20:07:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-03 20:24:06 +0100 |
| commit | 5d9eaa378277ed96456fec5a2037a8da4f38c8e0 (patch) | |
| tree | ca8aca465c51893aef9f8237338ef4e4aca472e5 /library/nametab.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 'library/nametab.ml')
0 files changed, 0 insertions, 0 deletions