diff options
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 ea2805b67..836568b89 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -492,13 +492,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) = @@ -654,7 +656,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) |