aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorHugo Herbelin2016-04-10 18:30:38 +0200
committerHugo Herbelin2016-04-27 21:55:45 +0200
commitf7ea0193c1aac918d8ed2df0d53df38dde5d1152 (patch)
treeb08efb7749b68952f311c22a4f7b0dcd55979cca /interp
parentdbe29599c2e9bf49368c7a92fe00259aa9cbbe15 (diff)
Not taking arguments given by name or position into account when
computing the arguments which allows to decide which list of implicit arguments to consider when several such lists are available.
Diffstat (limited to 'interp')
-rw-r--r--interp/constrintern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 072af07798..9304247a2b 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 l) imp in
+ let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) l)) imp in
let l = intern_impargs c env imp subscopes l in
smart_gapp c loc l