In "About", print all arguments, even if it is trailing list of _.

11 files changed, 35 insertions, 35 deletions

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..60944759c4 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -13,7 +13,7 @@ where
 ?y : [ |- nat]
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
-Arguments eq {A}%type_scope
+Arguments eq {A}%type_scope _ _
 Arguments eq_refl {B}%type_scope {y}, [B] _
 eq_refl : forall {A : Type} {x : A}, x = x
 
@@ -22,12 +22,12 @@ Arguments eq_refl {B}%type_scope {y}, [B] _
 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
+Arguments myEq _%type_scope _ _
+Arguments myrefl {C}%type_scope x _ : rename
 myrefl : forall {B : Type} (x : A), B -> myEq B x x
 
 myrefl is not universe polymorphic
-Arguments myrefl {C}%type_scope x : rename
+Arguments myrefl {C}%type_scope x _ : rename
 Expands to: Constructor Arguments_renaming.Test1.myrefl
 myplus = 
 fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
@@ -51,12 +51,12 @@ 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
+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
 
 myrefl is not universe polymorphic
-Arguments myrefl A%type_scope {C}%type_scope x : rename
+Arguments myrefl A%type_scope {C}%type_scope x _ : rename
 Expands to: Constructor Arguments_renaming.myrefl
 myrefl
      : forall (A C : Type) (x : A), C -> myEq A C x x
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..8c52e32bf6 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -1,19 +1,19 @@
 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 {A}%type_scope _ _
 Arguments eq_refl {A}%type_scope {x}, [A] _
 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,7 +80,7 @@ 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 {A}%type_scope _ _
 Arguments eq_refl {A}%type_scope {x}, {A} _
 n:nat
 
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/prettyp.ml b/vernac/prettyp.ml
index 2b46542287..d84165d032 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -268,8 +268,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 +294,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
@@ -336,7 +336,7 @@ let print_arguments ref =
   let moreimpls = List.map (fun (_,i) -> List.map 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