aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-05-12 18:10:34 +0200
committerPierre-Marie Pédrot2016-05-12 19:00:54 +0200
commit123504209e35b98ac14956ec6950cb7cd8b0089b (patch)
treeae2e3b31a7fa0dcded2862d18a486bee0c984d40 /kernel
parentc5de2c3a2aa96c468e7583577141a93e359a9baf (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')
0 files changed, 0 insertions, 0 deletions