aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2016-04-27 22:13:04 +0200
committerHugo Herbelin2016-04-27 22:13:04 +0200
commit78c0afc1b292a196f33bce1e7e21ae83084f9b71 (patch)
tree7c737eed6064ab403cec16fe1ff4c02d554758b7
parentce802a406e0667d02fb03571659ef7308fba3427 (diff)
Revert "Not taking arguments given by name or position into account when"
This reverts commit f7ea0193c1aac918d8ed2df0d53df38dde5d1152.
-rw-r--r--interp/constrintern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9304247a2b..072af07798 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1723,7 +1723,7 @@ let internalize globalenv env allow_patvar lvar c =
in aux 1 l subscopes eargs rargs
and apply_impargs c env imp subscopes l loc =
- let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) l)) imp in
+ let imp = select_impargs_size (List.length l) imp in
let l = intern_impargs c env imp subscopes l in
smart_gapp c loc l