diff options
| author | Pierre-Marie Pédrot | 2020-12-11 18:21:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-11 18:28:05 +0100 |
| commit | cade097ff6e5670b5f4c3ea832b593cf88251fbd (patch) | |
| tree | ee8f0fec90e56a21f6262bcc2b8423b94e1965b6 /kernel/type_errors.mli | |
| parent | 5a77078718c18b05e7ffb1366d6dd9e439ecfc91 (diff) | |
Fast path in tclPROGRESS.
We first check that the list of goals have the same length before trying to
engage into potentially costly equality checks.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions