Combine similar arguments when printing Arguments command

"similar" means sharing a scope or implicit status.

9 files changed, 64 insertions, 45 deletions

diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 6704337f80..f889da4e98 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,7 +1,7 @@
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch
+Arguments Nat.sub (_ _)%nat_scope : simpl nomatch
 The reduction tactics unfold Nat.sub but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
@@ -25,7 +25,7 @@ Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Arguments Nat.sub !_%nat_scope !_%nat_scope /
+Arguments Nat.sub (!_ !_)%nat_scope /
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor and when applied to 2 arguments
 Nat.sub is transparent
@@ -33,7 +33,7 @@ Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Arguments Nat.sub !_%nat_scope !_%nat_scope
+Arguments Nat.sub (!_ !_)%nat_scope
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor
 Nat.sub is transparent
@@ -43,14 +43,14 @@ 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
 fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 
 fcomp is not universe polymorphic
-Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ /
+Arguments fcomp {A B C}%type_scope _ _ _ /
 The reduction tactics unfold fcomp when applied to 6 arguments
 fcomp is transparent
 Expands to: Constant Arguments.fcomp
@@ -78,7 +78,7 @@ Expands to: Constant Arguments.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
+Arguments f [T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope
 The reduction tactics unfold f when the 4th, 5th and
   6th arguments evaluate to a constructor
 f is transparent
@@ -86,7 +86,7 @@ Expands to: Constant Arguments.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
+Arguments f [T1 T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope
 The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor
 f is transparent
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 53d5624f6f..5093e785de 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -13,21 +13,21 @@ 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] _
+Arguments eq {A}%type_scope
+Arguments eq_refl {B}%type_scope {y}, [B] _
 eq_refl : forall (A : Type) (x : A), x = x
 
 eq_refl is not universe polymorphic
-Arguments eq_refl {B%type_scope} {y}, [B] _
+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 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 :=
@@ -37,11 +37,11 @@ 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%nat_scope m%nat_scope : rename
+Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
 myplus : forall T : Type, T -> nat -> nat -> nat
 
 myplus is not universe polymorphic
-Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
+Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
 The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor
 myplus is transparent
@@ -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 _%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 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
@@ -68,11 +68,11 @@ 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%nat_scope m%nat_scope : rename
+Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
 myplus : forall T : Type, T -> nat -> nat -> nat
 
 myplus is not universe polymorphic
-Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
+Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
 The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor
 myplus is transparent
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 7489b8987e..e84ac85aa8 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 _%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 _%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
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index d65d2a8f55..5f22eb5d7c 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%nat_scope] [x0%nat_scope]
+Arguments d2 [x x0]%nat_scope
 map id (1 :: nil)
      : list nat
 map id' (1 :: nil)
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index ce058a6d34..da255e86cd 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,8 +1,8 @@
 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 _%type_scope
-Arguments exist2 [A%type_scope] _%function_scope _%function_scope
+Arguments sig2 [A]%type_scope (_ _)%type_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 2952b6d94b..4f09f00c56 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%type_scope} {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 7d0d81a3e8..71d162c314 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 sigT [A]%type_scope _%type_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}, [A] _
 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}, [A] _
 Expands to: Constructor Coq.Init.Logic.eq_refl
 eq_refl : forall (A : Type) (x : A), x = x
 
@@ -34,11 +34,11 @@ fix add (n m : nat) {struct n} : nat :=
   end
      : nat -> nat -> nat
 
-Arguments Nat.add _%nat_scope _%nat_scope
+Arguments Nat.add (_ _)%nat_scope
 Nat.add : nat -> nat -> nat
 
 Nat.add is not universe polymorphic
-Arguments Nat.add _%nat_scope _%nat_scope
+Arguments Nat.add (_ _)%nat_scope
 Nat.add is transparent
 Expands to: Constant Coq.Init.Nat.add
 Nat.add : nat -> nat -> nat
@@ -52,9 +52,9 @@ Expands to: Constant Coq.Init.Peano.plus_n_O
 Inductive le (n : nat) : nat -> Prop :=
     le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
 
-Arguments le _%nat_scope _%nat_scope
+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}, {A} _
 n:nat
 
 Hypothesis of the goal context.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 298a0789c4..525ca48bee 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -33,7 +33,7 @@ fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
      : forall A : Type@{u}, Wrap@{u} A -> A
 (* u |=  *)
 
-Arguments wrap {A%type_scope} {Wrap}
+Arguments wrap {A}%type_scope {Wrap}
 bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u *)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index ebdadc0865..080629ede2 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1075,10 +1075,28 @@ let string_of_definition_object_kind = let open Decls in function
               pr_smart_global q ++
               let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in
               let pr_if b x = if b then x else str "" in
-              let pr_br imp x = match imp with
-                | Impargs.Implicit -> str "[" ++ x ++ str "]"
-                | Impargs.MaximallyImplicit -> str "{" ++ x ++ str "}"
-                | Impargs.NotImplicit -> x in
+              let pr_one_arg (x,k) = pr_if k (str"!") ++ Name.print x in
+              let pr_br imp force x =
+                let left,right =
+                match imp with
+                | Impargs.Implicit -> str "[", str "]"
+                | Impargs.MaximallyImplicit -> str "{", str "}"
+                | Impargs.NotImplicit -> if force then str"(",str")" else mt(),mt()
+                in
+                left ++ x ++ right
+              in
+              let get_arguments_like s imp tl =
+                if s = None && imp = Impargs.NotImplicit then [], tl
+                else
+                  let rec fold extra = function
+                    | RealArg arg :: tl when
+                        Option.equal (fun a b -> String.equal a.CAst.v b.CAst.v) arg.notation_scope s
+                        && arg.implicit_status = imp ->
+                      fold ((arg.name,arg.recarg_like) :: extra) tl
+                    | args -> List.rev extra, args
+                  in
+                  fold [] tl
+              in
               let rec print_arguments = function
                   | [] -> mt()
                   | VolatileArg :: l -> spc () ++ str"/" ++ print_arguments l
@@ -1086,13 +1104,14 @@ let string_of_definition_object_kind = let open Decls in function
                   | RealArg { name = id; recarg_like = k;
                          notation_scope = s;
                          implicit_status = imp } :: tl ->
-                    spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++
-                    print_arguments tl
+                    let extra, tl = get_arguments_like s imp tl in
+                    spc() ++ pr_br imp (extra<>[]) (prlist_with_sep spc pr_one_arg ((id,k)::extra)) ++
+                    pr_s s ++ print_arguments tl
               in
               let rec print_implicits = function
                 | [] -> mt ()
                 | (name, impl) :: rest ->
-                   spc() ++ pr_br impl (Name.print name) ++ print_implicits rest
+                   spc() ++ pr_br impl false (Name.print name) ++ print_implicits rest
               in
               print_arguments args ++
                 if not (List.is_empty more_implicits) then