diff options
| author | Pierre-Marie Pédrot | 2017-03-26 22:28:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-03-27 12:05:14 +0200 |
| commit | 11b4703ed83eeda9d959464f08185aedd3f7c250 (patch) | |
| tree | 062409e8dbc6fa5a7540f7897d96ec680004f6b7 /kernel/type_errors.mli | |
| parent | 7fbf2a541fcc36e08ce595b482c2f257f171ab3d (diff) | |
More efficient check in validity of side-effects.
We don't need to look for the size of the whole list to find whether we can
extract a suffix from it, as we can do it in one go instead. This slowness
was observable in abstract-heavy code.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions