Merge PR #12875: Further extensions of About wrt Arguments and renaming

Reviewed-by: SkySkimmer
Ack-by: herbelin

17 files changed, 91 insertions, 68 deletions

diff --git a/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh b/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh
new file mode 100644
index 0000000000..bb08c13ef3
--- /dev/null
+++ b/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12875" ] || [ "$CI_BRANCH" = "master+about-print-all-arguments-names" ]; then
+
+    elpi_CI_REF=coq-master+adapt-coq12875-arguments-pass-name-impargs
+    elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
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.out b/test-suite/output/Arguments.out
index 8cf0797b17..5d1da05809 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -43,7 +43,7 @@ forall {D1 C1 : Type},
 (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
 
 pf is not universe polymorphic
-Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] : simpl never
+Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] _ _ : simpl never
 The reduction tactics never unfold pf
 pf is transparent
 Expands to: Constant Arguments.pf
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index c28bb14eb3..e46774f68a 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -13,21 +13,25 @@ where
 ?y : [ |- nat]
 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] _
-eq_refl : forall {A : Type} {x : A}, x = x
+Arguments eq {A}%type_scope _ _
+Arguments eq_refl {B}%type_scope {y}, [_] _
+  (where some original arguments have been renamed)
+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}, [_] _
+  (where some original arguments have been renamed)
 Expands to: Constructor Coq.Init.Logic.eq_refl
 Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x
 
-Arguments myEq _%type_scope
-Arguments myrefl {C}%type_scope x : rename
-myrefl : forall {B : Type} (x : A), B -> myEq B x x
+Arguments myEq _%type_scope _ _
+Arguments myrefl {C}%type_scope x _
+  (where some original arguments have been renamed)
+myrefl : forall {C : Type} (x : A), C -> myEq C x x
 
 myrefl is not universe polymorphic
-Arguments myrefl {C}%type_scope x : rename
+Arguments myrefl {C}%type_scope x _
+  (where some original arguments have been renamed)
 Expands to: Constructor Arguments_renaming.Test1.myrefl
 myplus = 
 fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
@@ -37,11 +41,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
-myplus : forall {T : Type}, T -> nat -> nat -> nat
+Arguments myplus {Z}%type_scope !t (!n m)%nat_scope
+  (where some original arguments have been renamed)
+myplus : forall {Z : Type}, Z -> nat -> nat -> nat
 
 myplus is not universe polymorphic
-Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
+Arguments myplus {Z}%type_scope !t (!n m)%nat_scope
+  (where some original arguments have been renamed)
 The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor
 myplus is transparent
@@ -51,12 +57,14 @@ Expands to: Constant Arguments_renaming.Test1.myplus
 Inductive myEq (A B : Type) (x : A) : A -> Prop :=
     myrefl : B -> myEq A B x x
 
-Arguments myEq (_ _)%type_scope
-Arguments myrefl A%type_scope {C}%type_scope x : rename
-myrefl : forall (A : Type) {B : Type} (x : A), B -> myEq A B x x
+Arguments myEq (_ _)%type_scope _ _
+Arguments myrefl A%type_scope {C}%type_scope x _
+  (where some original arguments have been renamed)
+myrefl : forall (A : Type) {C : Type} (x : A), C -> myEq A C x x
 
 myrefl is not universe polymorphic
-Arguments myrefl A%type_scope {C}%type_scope x : rename
+Arguments myrefl A%type_scope {C}%type_scope x _
+  (where some original arguments have been renamed)
 Expands to: Constructor Arguments_renaming.myrefl
 myrefl
      : forall (A C : Type) (x : A), C -> myEq A C x x
@@ -68,11 +76,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
-myplus : forall {T : Type}, T -> nat -> nat -> nat
+Arguments myplus {Z}%type_scope !t (!n m)%nat_scope
+  (where some original arguments have been renamed)
+myplus : forall {Z : Type}, Z -> nat -> nat -> nat
 
 myplus is not universe polymorphic
-Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
+Arguments myplus {Z}%type_scope !t (!n m)%nat_scope
+  (where some original arguments have been renamed)
 The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor
 myplus is transparent
@@ -87,6 +97,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/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 6976610b22..da2fc90fc3 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -7,7 +7,7 @@ fix F (t : t) : P t :=
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
 
-Arguments t_rect (_ _)%function_scope
+Arguments t_rect (_ _)%function_scope _
      = fun d : TT => match d with
                      | {| f3 := b |} => b
                      end
@@ -26,7 +26,7 @@ match Nat.eq_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
-Arguments proj (_ _)%nat_scope _%function_scope
+Arguments proj (_ _)%nat_scope _%function_scope _ _
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
   match l with
@@ -43,7 +43,7 @@ fun (A : Type) (x : I A) => match x with
                             end
      : forall A : Type, I A -> A
 
-Arguments uncast _%type_scope
+Arguments uncast _%type_scope _
 foo' = if A 0 then true else false
      : bool
 f = 
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index d8b88b8c1c..781e8e13a3 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
 d2 = fun x : nat => d1 (y:=x)
      : forall x x0 : nat, x0 = x -> x0 = x
 
-Arguments d2 [x x]%nat_scope
+Arguments d2 [x x]%nat_scope _
 map id (1 :: nil)
      : list nat
 map id' (1 :: nil)
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index e6c2806433..8e10107673 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -7,7 +7,7 @@ l : list' A
 Unable to unify "list' (A * A)%type" with "list' A".
 Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
 
-Arguments foo _%type_scope
-Arguments Foo _%type_scope
+Arguments foo _%type_scope _
+Arguments Foo _%type_scope _
 myprod unit bool
      : Set
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index da255e86cd..02e58775b5 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -2,7 +2,7 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
     exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}
 
 Arguments sig2 [A]%type_scope (_ _)%type_scope
-Arguments exist2 [A]%type_scope (_ _)%function_scope
+Arguments exist2 [A]%type_scope (_ _)%function_scope _ _ _
 exists x : nat, x = x
      : Prop
 fun b : bool => if b then b else b
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index bdfa8afb6a..b8daa69ad2 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -15,7 +15,7 @@ swap =
 fun (A B : Type) '(x, y) => (y, x)
      : forall A B : Type, A * B -> B * A
 
-Arguments swap {A B}%type_scope
+Arguments swap {A B}%type_scope _
 fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
      : forall A B : Type, A * B -> Prop
 forall (A B : Type) '(x, y), swap (x, y) = (y, x)
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 8fb267e343..fe16dba496 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -1,24 +1,24 @@
 existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 existT is template universe polymorphic on sigT.u0 sigT.u1
-Arguments existT [A]%type_scope _%function_scope
+Arguments existT [A]%type_scope _%function_scope _ _
 Expands to: Constructor Coq.Init.Specif.existT
 Inductive sigT (A : Type) (P : A -> Type) : Type :=
     existT : forall x : A, P x -> {x : A & P x}
 
 Arguments sigT [A]%type_scope _%type_scope
-Arguments existT [A]%type_scope _%function_scope
+Arguments existT [A]%type_scope _%function_scope _ _
 existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 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 {A}%type_scope _ _
+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
 
@@ -54,7 +54,7 @@ Inductive le (n : nat) : nat -> Prop :=
 
 Arguments le (_ _)%nat_scope
 Arguments le_n _%nat_scope
-Arguments le_S {n}%nat_scope [m]%nat_scope
+Arguments le_S {n}%nat_scope [m]%nat_scope _
 comparison : Set
 
 comparison is not universe polymorphic
@@ -80,8 +80,8 @@ Notation sym_eq := eq_sym
 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 {A}%type_scope _ _
+Arguments eq_refl {A}%type_scope {x}, {_} _
 n:nat
 
 Hypothesis of the goal context.
diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out
index 1dd89c9bcd..1cdb39b020 100644
--- a/test-suite/output/Projections.out
+++ b/test-suite/output/Projections.out
@@ -7,11 +7,11 @@ let B := A in fun (C : Type) (u : U A C) => (A, B, C, c _ _ u)
        let B := A in
        forall C : Type, U A C -> Type * Type * Type * (B * A * C)
 
-Arguments a (_ _)%type_scope
+Arguments a (_ _)%type_scope _
 b = 
 fun A : Type => let B := A in fun (C : Type) (u : U A C) => b _ _ u
      : forall A : Type,
        let B := A in
        forall (C : Type) (u : U A C), (A, B, C, c _ _ u) = (A, B, C, c _ _ u)
 
-Arguments b (_ _)%type_scope
+Arguments b (_ _)%type_scope _
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index edd2c9674f..163ed15606 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -5,24 +5,24 @@ Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
 
 PWrap has primitive projections with eta conversion.
 Arguments PWrap _%type_scope
-Arguments pwrap _%type_scope
+Arguments pwrap _%type_scope _
 punwrap@{u} = 
 fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
      : forall A : Type@{u}, PWrap@{u} A -> A
 (* u |=  *)
 
-Arguments punwrap _%type_scope
+Arguments punwrap _%type_scope _
 Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
 (* u |=  *)
 
 Arguments RWrap _%type_scope
-Arguments rwrap _%type_scope
+Arguments rwrap _%type_scope _
 runwrap@{u} = 
 fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap
      : forall A : Type@{u}, RWrap@{u} A -> A
 (* u |=  *)
 
-Arguments runwrap _%type_scope
+Arguments runwrap _%type_scope _
 Wrap@{u} = fun A : Type@{u} => A
      : Type@{u} -> Type@{u}
 (* u |=  *)
@@ -87,12 +87,12 @@ Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
 
 PWrap has primitive projections with eta conversion.
 Arguments PWrap _%type_scope
-Arguments pwrap _%type_scope
+Arguments pwrap _%type_scope _
 punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A
 (* K |=  *)
 
 punwrap is universe polymorphic
-Arguments punwrap _%type_scope
+Arguments punwrap _%type_scope _
 punwrap is transparent
 Expands to: Constant UnivBinders.punwrap
 The command has indeed failed with message:
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
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 2b46542287..8b00484b4a 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -75,12 +75,12 @@ let print_ref reduce ref udecl =
   let inst = Univ.make_abstract_instance univs in
   let bl = Printer.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
-  let typ = EConstr.of_constr typ in
   let typ =
     if reduce then
-      let ctx,ccl = Reductionops.splay_prod_assum env sigma typ
-      in EConstr.it_mkProd_or_LetIn ccl ctx
+      let ctx,ccl = Reductionops.splay_prod_assum env sigma (EConstr.of_constr typ)
+      in EConstr.to_constr sigma (EConstr.it_mkProd_or_LetIn ccl ctx)
     else typ in
+  let typ = Arguments_renaming.rename_type typ ref in
   let impargs = select_stronger_impargs (implicits_of_global ref) in
   let impargs = List.map binding_kind_of_status impargs in
   let variance = let open GlobRef in match ref with
@@ -95,7 +95,7 @@ let print_ref reduce ref udecl =
     else mt ()
   in
   let priv = None in (* We deliberately don't print private univs in About. *)
-  hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma ~impargs typ ++
+  hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma ~impargs typ ++
          Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv)
 
 (********************************)
@@ -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;
@@ -268,8 +272,10 @@ let dummy = {
   notation_scope = None;
 }
 
-let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} =
-  name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit
+let is_dummy = function
+  | Vernacexpr.(RealArg {implicit_status; name; recarg_like; notation_scope}) ->
+    name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit
+  | _ -> false
 
 let rec main_implicits i renames recargs scopes impls =
   if renames = [] && recargs = [] && scopes = [] && impls = [] then []
@@ -292,9 +298,7 @@ let rec main_implicits i renames recargs scopes impls =
     let tl = function [] -> [] | _::tl -> tl in
     (* recargs is special -> tl handled above *)
     let rest = main_implicits (i+1) (tl renames) recargs (tl scopes) (tl impls) in
-    if is_dummy status && rest = []
-    then [] (* we may have a trail of dummies due to eg "clear scopes" *)
-    else status :: rest
+    status :: rest
 
 let rec insert_fake_args volatile bidi impls =
   let open Vernacexpr in
@@ -320,11 +324,7 @@ let print_arguments ref =
     | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs
     | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs
   in
-  let flags, renames = match Arguments_renaming.arguments_names ref with
-    | exception Not_found -> flags, []
-    | [] -> flags, []
-    | renames -> `Rename::flags, renames
-  in
+  let renames = try Arguments_renaming.arguments_names ref with Not_found -> [] in
   let scopes = Notation.find_arguments_scope ref in
   let flags = if needs_extra_scopes ref scopes then `ExtraScopes::flags else flags in
   let impls = Impargs.extract_impargs_data (Impargs.implicits_of_global ref) in
@@ -333,15 +333,17 @@ 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 impls = [] && moreimpls = [] && flags = [] then []
+  if List.for_all is_dummy impls && moreimpls = [] && flags = [] then []
   else
     let open Constrexpr in
     let open Vernacexpr in
     [Ppvernac.pr_vernac_expr
-       (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags))]
+       (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags)) ++
+     (if renames = [] then mt () else
+      fnl () ++ str "  (where some original arguments have been renamed)")]
 
 let print_name_infos ref =
   let type_info_for_implicit =