diff options
| author | Pierre-Marie Pédrot | 2017-05-12 15:16:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-23 10:22:22 +0200 |
| commit | e22796a610853d8e7ff64785c98004d8ceac98e3 (patch) | |
| tree | 9fa94a7cbbfb08f001a065f44542180da23e5f53 /kernel/nativecode.ml | |
| parent | bf84180f963a31d1ec850d4ccedd599f2984ea9b (diff) | |
Postponing of universe constraints unification in term equality.
Instead of calling the universe unification at each term node, we accumulate
them and try to perform unification at the very end. This seems to be
experimentally faster.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions