diff options
| author | Maxime Dénès | 2016-10-28 09:29:25 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-28 09:29:25 +0200 |
| commit | 4f65c0370c5fc4163fa961a7fabb8e90fa7c45dd (patch) | |
| tree | 24a84ecb587edb6e14a1e1469f604239b7a6d6c2 /library | |
| parent | d500a684be14b0c781ea4cda0ee02d3c5cdcad81 (diff) | |
| parent | ebb5bd7c2048daa7241bb07d8b53d07e0be27e62 (diff) | |
Merge remote-tracking branch 'github/pr/337' into v8.6
Was PR#337: Fix arguments
Diffstat (limited to 'library')
| -rw-r--r-- | library/impargs.ml | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index bce7a15cbe..828d652c83 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -491,13 +491,15 @@ let implicits_of_global ref = let l = Refmap.find ref !implicits_table in try let rename_l = Arguments_renaming.arguments_names ref in - let rename imp name = match imp, name with - | Some (_, x,y), Name id -> Some (id, x,y) - | _ -> imp in - List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l + let rec rename implicits names = match implicits, names with + | [], _ -> [] + | _, [] -> implicits + | Some (_, x,y) :: implicits, Name id :: names -> + Some (id, x,y) :: rename implicits names + | imp :: implicits, _ :: names -> imp :: rename implicits names + in + List.map (fun (t, il) -> t, rename il rename_l) l with Not_found -> l - | Invalid_argument _ -> - anomaly (Pp.str "renamings list and implicits list have different lenghts") with Not_found -> [DefaultImpArgs,[]] let cache_implicits_decl (ref,imps) = @@ -657,7 +659,7 @@ let check_inclusion l = let rec aux = function | n1::(n2::_ as nl) -> if n1 <= n2 then - error "Sequences of implicit arguments must be of different lengths"; + error "Sequences of implicit arguments must be of different lengths."; aux nl | _ -> () in aux (List.map (fun (imps,_) -> List.length imps) l) |