diff options
| author | Pierre-Marie Pédrot | 2019-04-29 18:50:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-03 13:42:40 +0200 |
| commit | 24c570834dccc90c7ff14d3f6b9d33b818fa79c9 (patch) | |
| tree | d986ebd93114b8b29711e8afc1811683905d4812 /kernel/type_errors.mli | |
| parent | 6960da4736186fa6214854329f36f558e7aa4d0b (diff) | |
Fix #9994: `revert dependent` is extremely slow.
We add a fast path when generalizing over variables.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions