diff options
| author | Pierre-Marie Pédrot | 2016-08-05 12:38:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-06 12:06:34 +0200 |
| commit | f1e1b7f735c8cd4a1f3cc52e7f9a7cdf1481ffe5 (patch) | |
| tree | d9c24d91ab1a3ed14e72ec6aa0e6ccd5d55b0d4d /pretyping/pretype_errors.ml | |
| parent | 26e5194bc252e4ac71c74f8ac73a0e2cbe82edf6 (diff) | |
Using a dedicated kind of substitutions in evar name generation.
This saves a quadratic allocation by replacing arrays with maps.
Diffstat (limited to 'pretyping/pretype_errors.ml')
0 files changed, 0 insertions, 0 deletions