diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/recordops.ml | 2 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 2 |
2 files changed, 2 insertions, 2 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) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index deb03f516..c44fbc0ba 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -436,7 +436,7 @@ let instance_constructor (cl,u) args = | None -> true | Some _ -> false in - let lenpars = List.length (List.filter filter (snd cl.cl_context)) in + let lenpars = List.count filter (snd cl.cl_context) in let pars = fst (List.chop lenpars args) in match cl.cl_impl with | IndRef ind -> |