diff options
| author | Pierre-Marie Pédrot | 2020-02-03 13:51:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-03 15:01:02 +0100 |
| commit | db2289c50c358ac5bf7c2d2be7b9d255b20173ef (patch) | |
| tree | f2397c32777aaa498252f6b9f3539c4894cde23f /kernel/indTyping.ml | |
| parent | 1c1c04d0e3e02ce461fb953f08e2d8c68e52ee63 (diff) | |
Delay lifting in Evarsolve aliasing.
It turns out that eagerly computing the lift of huge terms when it is not
used is not great for performance.
Fixes part of #11488.
Diffstat (limited to 'kernel/indTyping.ml')
0 files changed, 0 insertions, 0 deletions