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 /printing/prettyp.ml | |
| parent | 1a8a8db7a9e4eb5ab56cd192411529661a4972c7 (diff) | |
Do not compose List.length with List.filter.
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 84649e6eb..08228cb20 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -132,7 +132,7 @@ let print_renames_list prefix l = let need_expansion impl ref = let typ = Global.type_of_global_unsafe ref in let ctx = prod_assum typ in - let nprods = List.length (List.filter (fun (_,b,_) -> Option.is_empty b) ctx) in + let nprods = List.count (fun (_,b,_) -> Option.is_empty b) ctx in not (List.is_empty impl) && List.length impl >= nprods && let _,lastimpl = List.chop nprods impl in List.exists is_status_implicit lastimpl |