When reporting an implicit argument error on a rename argument, use the renaming.

Example:

> Arguments id [B] {b} : rename.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Argument B is a trailing implicit, so it can't be declared non
maximal. Please use { } instead of [ ].

6 files changed, 13 insertions, 8 deletions

diff --git a/interp/impargs.ml b/interp/impargs.ml
index 48961c6c8a..7742f985de 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -667,10 +667,12 @@ let explicit_kind i = function
 
 let compute_implicit_statuses autoimps l =
   let rec aux i = function
-    | _ :: autoimps, Explicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
-    | na :: autoimps, MaxImplicit :: manualimps ->
+    | _ :: autoimps, (_, Explicit) :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
+    | na :: autoimps, (Anonymous, MaxImplicit) :: manualimps
+    | _ :: autoimps, (na, MaxImplicit) :: manualimps ->
        Some (explicit_kind i na, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
-    | na :: autoimps, NonMaxImplicit :: manualimps ->
+    | na :: autoimps, (Anonymous, NonMaxImplicit) :: manualimps
+    | _ :: autoimps, (na, NonMaxImplicit) :: manualimps ->
        let imps' = aux (i+1) (autoimps, manualimps) in
        let max = set_maximality Error na i imps' false in
        Some (explicit_kind i na, Manual, (max, true)) :: imps'
@@ -693,7 +695,7 @@ let set_implicits local ref l =
        check_rigidity (is_rigid env sigma t);
        (* Sort by number of implicits, decreasing *)
        let is_implicit = function
-         | Explicit -> false
+         | _, Explicit -> false
          | _ -> true in
        let l = List.map (fun imps -> (imps,List.count is_implicit imps)) l in
        let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 97841b37f2..c8bcef19c8 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -117,7 +117,7 @@ val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
 (** [set_implicits local ref l]
    Manual declaration of implicit arguments.
   `l` is a list of possible sequences of implicit statuses. *)
-val set_implicits : bool -> GlobRef.t -> Glob_term.binding_kind list list -> unit
+val set_implicits : bool -> GlobRef.t -> (Name.t * Glob_term.binding_kind) list list -> unit
 
 val implicits_of_global : GlobRef.t -> implicits_list list
 
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 24772a8514..4a907b2795 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -159,7 +159,7 @@ let declare_one_prenex_implicit locality f =
   | [] ->
     errorstrm (str "Expected some implicits for " ++ pr_qualid f)
   | impls ->
-    Impargs.set_implicits locality fref [impls]
+    Impargs.set_implicits locality fref [List.map (fun imp -> (Anonymous,imp)) impls]
 
 }
 
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 60944759c4..533e64f5b4 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -87,6 +87,9 @@ The command has indeed failed with message:
 Argument number 3 is a trailing implicit, so it can't be declared non
 maximal. Please use { } instead of [ ].
 The command has indeed failed with message:
+Argument z is a trailing implicit, so it can't be declared non maximal.
+Please use { } instead of [ ].
+The command has indeed failed with message:
 Extra arguments: y.
 The command has indeed failed with message:
 Flag "rename" expected to rename A into R.
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index 6001850046..13bda0c070 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -48,6 +48,7 @@ Check @myplus.
 
 Fail Arguments eq_refl {F g}, [H] k.
 Fail Arguments eq_refl {F}, [F] : rename.
+Fail Arguments eq {A} x [_] : rename.
 Fail Arguments eq {A} x [z] : rename.
 Fail Arguments eq {F} x z y.
 Fail Arguments eq {R} s t.
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index be9cc059a7..adf1f42beb 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -218,9 +218,8 @@ let vernac_arguments ~section_local reference args more_implicits flags =
   in
   let implicits = implicits :: more_implicits in
 
-  let implicits = List.map (List.map snd) implicits in
   let implicits_specified = match implicits with
-    | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l
+    | [l] -> List.exists (function _, Glob_term.Explicit -> false | _ -> true) l
     | _ -> true in
 
   if implicits_specified && clear_implicits_flag then