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 /pretyping/recordops.ml | |
| parent | 1a8a8db7a9e4eb5ab56cd192411529661a4972c7 (diff) | |
Do not compose List.length with List.filter.
Diffstat (limited to 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 7fde7b7ac..af4865401 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -299,7 +299,7 @@ let check_and_decompose_canonical_structure ref = | Construct ((indsp,1),u) -> indsp | _ -> error_not_structure ref in let s = try lookup_structure indsp with Not_found -> error_not_structure ref in - let ntrue_projs = List.length (List.filter (fun (_, x) -> x) s.s_PROJKIND) in + let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then error_not_structure ref; (sp,indsp) |