Merge PR #11146: Combine similar arguments when printing Arguments command

Reviewed-by: ejgallego
Reviewed-by: herbelin

15 files changed, 127 insertions, 92 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/comArguments.ml b/vernac/comArguments.ml
index 737e0427ec..15077298aa 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -60,7 +60,7 @@ let warn_arguments_assert =
 (* [nargs_for_red] is the number of arguments required to trigger reduction,
    [args] is the main list of arguments statuses,
    [more_implicits] is a list of extra lists of implicit statuses  *)
-let vernac_arguments ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags =
+let vernac_arguments ~section_local reference args more_implicits flags =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let assert_flag = List.mem `Assert flags in
@@ -83,6 +83,23 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
   if clear_implicits_flag && default_implicits_flag then
     err_incompat "clear implicits" "default implicits";
 
+  let args, nargs_for_red, nargs_before_bidi, _i =
+    List.fold_left (fun (args,red,bidi,i) arg ->
+        match arg with
+        | RealArg arg -> (arg::args,red,bidi,i+1)
+        | VolatileArg ->
+          if Option.has_some red
+          then CErrors.user_err Pp.(str "The \"/\" modifier may only occur once.");
+          (args,Some i,bidi,i)
+        | BidiArg ->
+          if Option.has_some bidi
+          then CErrors.user_err Pp.(str "The \"&\" modifier may only occur once.");
+          (args,red,Some i,i))
+      ([],None,None,0)
+      args
+  in
+  let args = List.rev args in
+
   let sr = smart_global reference in
   let inf_names =
     let ty, _ = Typeops.type_of_global_in_context env sr in
diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli
index f78e01a11f..71effddf67 100644
--- a/vernac/comArguments.mli
+++ b/vernac/comArguments.mli
@@ -13,7 +13,5 @@ val vernac_arguments
   -> Libnames.qualid Constrexpr.or_by_notation
   -> Vernacexpr.vernac_argument_status list
   -> (Names.Name.t * Impargs.implicit_kind) list list
-  -> int option
-  -> int option
   -> Vernacexpr.arguments_modifier list
   -> unit
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 0515e88a15..5b97e06b2b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -781,25 +781,8 @@ GRAMMAR EXTEND Gram
           ];
         mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> { l } ] ->
          { let mods = match mods with None -> [] | Some l -> List.flatten l in
-         let slash_position = ref None in
-         let ampersand_position = ref None in
-         let rec parse_args i = function
-           | [] -> []
-           | `Id x :: args -> x :: parse_args (i+1) args
-           | `Slash :: args ->
-              if Option.is_empty !slash_position then
-                (slash_position := Some i; parse_args i args)
-              else
-                user_err Pp.(str "The \"/\" modifier can occur only once")
-           | `Ampersand :: args ->
-             if Option.is_empty !ampersand_position then
-               (ampersand_position := Some i; parse_args i args)
-             else
-               user_err Pp.(str "The \"&\" modifier can occur only once")
-         in
-         let args = parse_args 0 (List.flatten args) in
          let more_implicits = Option.default [] more_implicits in
-         VernacArguments (qid, args, more_implicits, !slash_position, !ampersand_position, mods) }
+         VernacArguments (qid, List.flatten args, more_implicits, mods) }
 
       | IDENT "Implicit"; "Type"; bl = reserv_list ->
            { VernacReserve bl }
@@ -843,17 +826,17 @@ GRAMMAR EXTEND Gram
   argument_spec_block: [
     [ item = argument_spec ->
       { let name, recarg_like, notation_scope = item in
-      [`Id { name=name; recarg_like=recarg_like;
+      [RealArg { name=name; recarg_like=recarg_like;
              notation_scope=notation_scope;
              implicit_status = NotImplicit}] }
-    | "/" -> { [`Slash] }
-    | "&" -> { [`Ampersand] }
+    | "/" -> { [VolatileArg] }
+    | "&" -> { [BidiArg] }
     | "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter ->
        { let f x = match sc, x with
          | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
          | Some _, Some _ -> user_err Pp.(str "scope declared twice") in
        List.map (fun (name,recarg_like,notation_scope) ->
-           `Id { name=name; recarg_like=recarg_like;
+           RealArg { name=name; recarg_like=recarg_like;
                  notation_scope=f notation_scope;
                  implicit_status = NotImplicit}) items }
     | "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter ->
@@ -861,7 +844,7 @@ GRAMMAR EXTEND Gram
          | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
          | Some _, Some _ -> user_err Pp.(str "scope declared twice") in
        List.map (fun (name,recarg_like,notation_scope) ->
-           `Id { name=name; recarg_like=recarg_like;
+           RealArg { name=name; recarg_like=recarg_like;
                  notation_scope=f notation_scope;
                  implicit_status = Implicit}) items }
     | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter ->
@@ -869,7 +852,7 @@ GRAMMAR EXTEND Gram
          | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
          | Some _, Some _ -> user_err Pp.(str "scope declared twice") in
        List.map (fun (name,recarg_like,notation_scope) ->
-           `Id { name=name; recarg_like=recarg_like;
+           RealArg { name=name; recarg_like=recarg_like;
                  notation_scope=f notation_scope;
                  implicit_status = MaximallyImplicit}) items }
     ]
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 3dbf7afb78..080629ede2 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1068,39 +1068,52 @@ let string_of_definition_object_kind = let open Decls in function
                 | Some Flags.Current -> [SetOnlyParsing]
                 | Some v -> [SetCompatVersion v]))
         )
-      | VernacArguments (q, args, more_implicits, nargs, nargs_before_bidi, mods) ->
+      | VernacArguments (q, args, more_implicits, mods) ->
         return (
           hov 2 (
             keyword "Arguments" ++ spc() ++
               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 rec print_arguments n nbidi l =
-                match n, nbidi, l with
-                  | Some 0, _, l -> spc () ++ str"/" ++ print_arguments None nbidi l
-                  | _, Some 0, l -> spc () ++ str"&" ++ print_arguments n None l
-                  | None, None, [] -> mt()
-                  | _, _, [] ->
-                    let dummy = {name=Anonymous; recarg_like=false;
-                                 notation_scope=None; implicit_status=Impargs.NotImplicit}
-                    in
-                    print_arguments n nbidi [dummy]
-                  | n, nbidi, { name = id; recarg_like = k;
+              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
+                  | BidiArg :: l -> spc () ++ str"&" ++ print_arguments l
+                  | 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 (Option.map pred n) (Option.map pred nbidi) 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 nargs nargs_before_bidi args ++
+              print_arguments args ++
                 if not (List.is_empty more_implicits) then
                   prlist (fun l -> str"," ++ print_implicits l) more_implicits
                 else (mt ()) ++
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 5ebc89892c..ea49cae9db 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -259,6 +259,13 @@ let implicit_kind_of_status = function
   | None -> Anonymous, NotImplicit
   | Some (id,_,(maximal,_)) -> Name id, if maximal then MaximallyImplicit else Implicit
 
+let dummy = {
+  Vernacexpr.implicit_status = NotImplicit;
+  name = Anonymous;
+  recarg_like = false;
+  notation_scope = None;
+}
+
 let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} =
   name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit
 
@@ -287,6 +294,20 @@ let rec main_implicits i renames recargs scopes impls =
     then [] (* we may have a trail of dummies due to eg "clear scopes" *)
     else status :: rest
 
+let rec insert_fake_args volatile bidi impls =
+  let open Vernacexpr in
+  match volatile, bidi with
+  | Some 0, _ -> VolatileArg :: insert_fake_args None bidi impls
+  | _, Some 0 -> BidiArg :: insert_fake_args volatile None impls
+  | None, None -> List.map (fun a -> RealArg a) impls
+  | _, _ ->
+    let hd, tl = match impls with
+      | impl :: impls -> impl, impls
+      | [] -> dummy, []
+    in
+    let f = Option.map pred in
+    RealArg hd :: insert_fake_args (f volatile) (f bidi) tl
+
 let print_arguments ref =
   let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in
   let flags, recargs, nargs_for_red =
@@ -312,12 +333,13 @@ let print_arguments ref =
   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 bidi = Pretyping.get_bidirectionality_hint ref in
-  if impls = [] && moreimpls = [] && nargs_for_red = None && bidi = None && flags = [] then []
+  let impls = insert_fake_args nargs_for_red bidi impls in
+  if impls = [] && moreimpls = [] && flags = [] then []
   else
     let open Constrexpr in
     let open Vernacexpr in
     [Ppvernac.pr_vernac_expr
-       (VernacArguments (CAst.make (AN qid), impls, moreimpls, nargs_for_red, bidi, flags))]
+       (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags))]
 
 let print_name_infos ref =
   let type_info_for_implicit =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f56cc00c3b..535aceed15 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2167,10 +2167,10 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
         vernac_hints ~atts dbnames hints)
   | VernacSyntacticDefinition (id,c,b) ->
      VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
-  | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) ->
+  | VernacArguments (qid, args, more_implicits, flags) ->
     VtDefault(fun () ->
         with_section_locality ~atts
-          (ComArguments.vernac_arguments qid args more_implicits nargs bidi flags))
+          (ComArguments.vernac_arguments qid args more_implicits flags))
   | VernacReserve bl ->
     VtDefault(fun () ->
         unsupported_attributes atts;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 564c55670d..ce96d9265c 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -250,13 +250,17 @@ type vernac_cumulative = VernacCumulative | VernacNonCumulative
 
 (** {6 The type of vernacular expressions} *)
 
-type vernac_argument_status = {
+type vernac_one_argument_status = {
   name : Name.t;
   recarg_like : bool;
   notation_scope : string CAst.t option;
   implicit_status : Impargs.implicit_kind;
 }
 
+type vernac_argument_status =
+  | VolatileArg | BidiArg
+  | RealArg of vernac_one_argument_status
+
 type arguments_modifier =
   [  `Assert
   | `ClearBidiHint
@@ -383,8 +387,6 @@ type nonrec vernac_expr =
       qualid or_by_notation *
       vernac_argument_status list (* Main arguments status list *) *
       (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
-      int option (* Number of args to trigger reduction *) *
-      int option (* Number of args before bidirectional typing *) *
       arguments_modifier list
   | VernacReserve of simple_binder list
   | VernacGeneralizable of (lident list) option