diff options
| author | Arnaud Spiwack | 2014-10-21 12:25:11 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-22 07:31:45 +0200 |
| commit | 328c775067b045b851ec48b97f0507afcc4bb768 (patch) | |
| tree | 0fe3cdf8dfecc09cffc1da721d91e97d1ec7c77c /dev | |
| parent | e87a491d724c83fe1bc98dfb94c665e8ba7f56a1 (diff) | |
Proofview: use an iter-like combinator rather than a fold_left-like one for dispatch.
Leads to clearer an more efficient code.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions