diff options
| author | Guillaume Melquiond | 2016-08-09 16:29:41 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-08-09 16:34:39 +0200 |
| commit | c35ad7b248b59964a55d6e5be86a604e4268bf4c (patch) | |
| tree | cfab63128164277f1ded5c37924dd08e7a986b9e /kernel | |
| parent | dabe6d0e1d1782d3e9647e04aa1bf161765ad882 (diff) | |
Make List.map_filter(_i) tail-recursive.
While the performance gain should go unnoticed in most cases, in some
degenerate situations, e.g. the evar-stressing test-case of bug #4964,
this commit speeds up coq by 10% since most of the time is spent scanning
long lists with most of the elements filtered out.
Note that this commit also changes the scanning order to front-to-back,
which is a bit less surprising (though no code should ever depend on the
scanning order).
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions