Merge branch 'v8.6'

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)