diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-26 10:07:19 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-31 17:01:51 +0100 |
| commit | 1a157442dff4bfa127af467c49280e79889acde7 (patch) | |
| tree | 7d10a0093e75b652c7cce79920c054d4c2f41c91 /kernel/mod_typing.ml | |
| parent | 1a8a8db7a9e4eb5ab56cd192411529661a4972c7 (diff) | |
Do not compose List.length with List.filter.
Diffstat (limited to 'kernel/mod_typing.ml')
0 files changed, 0 insertions, 0 deletions