diff options
| author | Pierre-Marie Pédrot | 2016-05-12 18:10:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-12 19:00:54 +0200 |
| commit | 123504209e35b98ac14956ec6950cb7cd8b0089b (patch) | |
| tree | ae2e3b31a7fa0dcded2862d18a486bee0c984d40 /kernel/nativecode.ml | |
| parent | c5de2c3a2aa96c468e7583577141a93e359a9baf (diff) | |
Small optimization in evar resolution.
Instead of rebuilding a whole set of evars just to make a typeclass filter,
we use the source evarmap.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions