diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-10 18:30:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:45 +0200 |
| commit | f7ea0193c1aac918d8ed2df0d53df38dde5d1152 (patch) | |
| tree | b08efb7749b68952f311c22a4f7b0dcd55979cca /interp | |
| parent | dbe29599c2e9bf49368c7a92fe00259aa9cbbe15 (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.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 072af0779..9304247a2 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 |