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.

2 files changed, 5 insertions, 5 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.