Where there are several lists of implicit arguments, don't pretend names matter.

That is, in "About", use _ for the variables of the extra lists.

See discussion at https://github.com/coq/coq/pull/12875#issuecomment-679190489.

3 files changed, 10 insertions, 6 deletions

diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 8cc4383f49..d56cd4d610 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -14,11 +14,11 @@ where
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 Arguments eq {A}%type_scope _ _
-Arguments eq_refl {B}%type_scope {y}, [B] _
+Arguments eq_refl {B}%type_scope {y}, [_] _
 eq_refl : forall {B : Type} {y : B}, y = y
 
 eq_refl is not universe polymorphic
-Arguments eq_refl {B}%type_scope {y}, [B] _
+Arguments eq_refl {B}%type_scope {y}, [_] _
 Expands to: Constructor Coq.Init.Logic.eq_refl
 Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x
 
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 8c52e32bf6..fe16dba496 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -14,11 +14,11 @@ Argument A is implicit
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 Arguments eq {A}%type_scope _ _
-Arguments eq_refl {A}%type_scope {x}, [A] _
+Arguments eq_refl {A}%type_scope {x}, [_] _
 eq_refl : forall {A : Type} {x : A}, x = x
 
 eq_refl is not universe polymorphic
-Arguments eq_refl {A}%type_scope {x}, [A] _
+Arguments eq_refl {A}%type_scope {x}, [_] _
 Expands to: Constructor Coq.Init.Logic.eq_refl
 eq_refl : forall {A : Type} {x : A}, x = x
 
@@ -81,7 +81,7 @@ Expands to: Notation Coq.Init.Logic.sym_eq
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 Arguments eq {A}%type_scope _ _
-Arguments eq_refl {A}%type_scope {x}, {A} _
+Arguments eq_refl {A}%type_scope {x}, {_} _
 n:nat
 
 Hypothesis of the goal context.
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 037ad7db1d..7ceaa5a1bc 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -261,6 +261,10 @@ let implicit_kind_of_status = function
   | None -> Anonymous, Glob_term.Explicit
   | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit
 
+let extra_implicit_kind_of_status imp =
+  let _,imp = implicit_kind_of_status imp in
+  (Anonymous, imp)
+
 let dummy = {
   Vernacexpr.implicit_status = Glob_term.Explicit;
   name = Anonymous;
@@ -329,7 +333,7 @@ let print_arguments ref =
     | [] -> assert false
   in
   let impls = main_implicits 0 renames recargs scopes impls in
-  let moreimpls = List.map (fun (_,i) -> List.map implicit_kind_of_status i) moreimpls in
+  let moreimpls = List.map (fun (_,i) -> List.map extra_implicit_kind_of_status i) moreimpls in
   let bidi = Pretyping.get_bidirectionality_hint ref in
   let impls = insert_fake_args nargs_for_red bidi impls in
   if List.for_all is_dummy impls && moreimpls = [] && flags = [] then []