diff options
| author | Pierre-Marie Pédrot | 2017-06-07 17:07:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-01 12:04:59 +0200 |
| commit | 420c919854f50b9f9d47ba8299dc27f0df051d30 (patch) | |
| tree | b5f75108a039efa92bd3875960997f9e5a82b684 /kernel/nativecode.ml | |
| parent | 3072bd9d080984833f5eb007bf15c6e9305619e3 (diff) | |
Do not hashcons universes beforehand.
This should save a lot of useless reallocations and hashset crawling, which
end up costing a lot.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions