aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses.ml')
-rw-r--r--pretyping/typeclasses.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index deb03f5160..c44fbc0ba8 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 ->