Fix output tests

12 files changed, 81 insertions, 164 deletions

diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 3c1e27ba9d..7bfb2fc210 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,41 +1,31 @@
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
-The reduction tactics unfold Nat.sub but avoid exposing match constructs
+Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
-The reduction tactics unfold Nat.sub when applied to 1 argument
-  but avoid exposing match constructs
+Arguments Nat.sub _%nat_scope / _%nat_scope : simpl nomatch
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
-The reduction tactics unfold Nat.sub
-  when the 1st argument evaluates to a constructor and
-  when applied to 1 argument but avoid exposing match constructs
+Arguments Nat.sub !_%nat_scope / _%nat_scope : simpl nomatch
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
-The reduction tactics unfold Nat.sub when the 1st and
-  2nd arguments evaluate to a constructor and when applied to 2 arguments
+Arguments Nat.sub !_%nat_scope !_%nat_scope /
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
-The reduction tactics unfold Nat.sub when the 1st and
-  2nd arguments evaluate to a constructor
+Arguments Nat.sub !_%nat_scope !_%nat_scope
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 pf :
@@ -43,57 +33,43 @@ forall D1 C1 : Type,
 (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
 
 pf is not universe polymorphic
-Arguments D2, C2 are implicit
-Arguments D1, C1 are implicit and maximally inserted
-Argument scopes are [foo_scope type_scope _ _ _ _ _]
-The reduction tactics never unfold pf
+Arguments pf {D1%foo_scope} {C1%type_scope} _ [D2] [C2] : simpl never
 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 A, B, C are implicit and maximally inserted
-Argument scopes are [type_scope type_scope type_scope _ _ _]
-The reduction tactics unfold fcomp when applied to 6 arguments
+Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ /
 fcomp is transparent
 Expands to: Constant Arguments.fcomp
 volatile : nat -> nat
 
 volatile is not universe polymorphic
-Argument scope is [nat_scope]
-The reduction tactics always unfold volatile
+Arguments volatile / _%nat_scope
 volatile is transparent
 Expands to: Constant Arguments.volatile
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Argument scopes are [_ _ nat_scope _ nat_scope]
+Arguments f _ _ _%nat_scope _ _%nat_scope
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Argument scopes are [_ _ nat_scope _ nat_scope]
-The reduction tactics unfold f when the 3rd, 4th and
-  5th arguments evaluate to a constructor
+Arguments f _ _ !_%nat_scope !_ !_%nat_scope
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Argument T2 is implicit
-Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
-The reduction tactics unfold f when the 4th, 5th and
-  6th arguments evaluate to a constructor
+Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
 f is transparent
 Expands to: Constant Arguments.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Arguments T1, T2 are implicit
-Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
-The reduction tactics unfold f when the 5th, 6th and
-  7th arguments evaluate to a constructor
+Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
 f is transparent
 Expands to: Constant Arguments.f
      = forall v : unit, f 0 0 5 v 3 = 2
@@ -103,8 +79,7 @@ Expands to: Constant Arguments.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-The reduction tactics unfold f when the 5th, 6th and
-  7th arguments evaluate to a constructor
+Arguments f _ _ _ _ !_ !_ !_
 f is transparent
 Expands to: Constant Arguments.f
 forall w : r, w 3 true = tt
@@ -118,9 +93,7 @@ Extra arguments: _, _.
 volatilematch : nat -> nat
 
 volatilematch is not universe polymorphic
-Argument scope is [nat_scope]
-The reduction tactics always unfold volatilematch
-  but avoid exposing match constructs
+Arguments volatilematch / _%nat_scope : simpl nomatch
 volatilematch is transparent
 Expands to: Constant Arguments.volatilematch
      = fun n : nat => volatilematch n
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 69ba329ff1..7b25fd40f8 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -1,29 +1,29 @@
 a : bool -> bool
 
 a is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments a _%bool_scope
 Expands to: Variable a
 b : bool -> bool
 
 b is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments b _%bool_scope
 Expands to: Variable b
 negb'' : bool -> bool
 
 negb'' is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments negb'' _%bool_scope
 negb'' is transparent
 Expands to: Constant ArgumentsScope.A.B.negb''
 negb' : bool -> bool
 
 negb' is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments negb' _%bool_scope
 negb' is transparent
 Expands to: Constant ArgumentsScope.A.negb'
 negb : bool -> bool
 
 negb is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments negb _%bool_scope
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 a : bool -> bool
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 65c902202d..e025c167e3 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -13,36 +13,21 @@ where
 ?y : [ |- nat]
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
-For eq_refl: Arguments are renamed to B, y
-For eq: Argument A is implicit and maximally inserted
-For eq_refl, when applied to no arguments:
-  Arguments B, y are implicit and maximally inserted
-For eq_refl, when applied to 1 argument:
-  Argument B is implicit
-For eq: Argument scopes are [type_scope _ _]
-For eq_refl: Argument scopes are [type_scope _]
+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 are renamed to B, y
-When applied to no arguments:
-  Arguments B, y are implicit and maximally inserted
-When applied to 1 argument:
-  Argument B is implicit
-Argument scopes are [type_scope _]
+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
 
-For myrefl: Arguments are renamed to C, x, _
-For myrefl: Argument C is implicit and maximally inserted
-For myEq: Argument scopes are [type_scope _ _]
-For myrefl: Argument scopes are [type_scope _ _]
+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 are renamed to C, x, _
-Argument C is implicit and maximally inserted
-Argument scopes are [type_scope _ _]
+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 :=
@@ -52,17 +37,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-Arguments are renamed to Z, t, n, m
-Argument Z is implicit and maximally inserted
-Argument scopes are [type_scope _ nat_scope nat_scope]
+Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
 myplus : forall T : Type, T -> nat -> nat -> nat
 
 myplus is not universe polymorphic
-Arguments are renamed to Z, t, n, m
-Argument Z is implicit and maximally inserted
-Argument scopes are [type_scope _ nat_scope nat_scope]
-The reduction tactics unfold myplus when the 2nd and
-  3rd arguments evaluate to a constructor
+Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
 myplus is transparent
 Expands to: Constant Arguments_renaming.Test1.myplus
 @myplus
@@ -70,16 +49,12 @@ Expands to: Constant Arguments_renaming.Test1.myplus
 Inductive myEq (A B : Type) (x : A) : A -> Prop :=
     myrefl : B -> myEq A B x x
 
-For myrefl: Arguments are renamed to A, C, x, _
-For myrefl: Argument C is implicit and maximally inserted
-For myEq: Argument scopes are [type_scope type_scope _ _]
-For myrefl: Argument scopes are [type_scope type_scope _ _]
+Arguments myEq _%type_scope _%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 are renamed to A, C, x, _
-Argument C is implicit and maximally inserted
-Argument scopes are [type_scope type_scope _ _]
+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
@@ -91,17 +66,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-Arguments are renamed to Z, t, n, m
-Argument Z is implicit and maximally inserted
-Argument scopes are [type_scope _ nat_scope nat_scope]
+Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
 myplus : forall T : Type, T -> nat -> nat -> nat
 
 myplus is not universe polymorphic
-Arguments are renamed to Z, t, n, m
-Argument Z is implicit and maximally inserted
-Argument scopes are [type_scope _ nat_scope nat_scope]
-The reduction tactics unfold myplus when the 2nd and
-  3rd arguments evaluate to a constructor
+Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
 myplus is transparent
 Expands to: Constant Arguments_renaming.myplus
 @myplus
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index cb835ab48d..7489b8987e 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
 
-Argument scopes are [function_scope function_scope _]
+Arguments t_rect _%function_scope _%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
 
-Argument scopes are [nat_scope nat_scope function_scope _ _]
+Arguments proj _%nat_scope _%nat_scope _%function_scope
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
   match l with
@@ -36,14 +36,14 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
   end
      : forall A : Type, list A -> option A
 
-Argument scopes are [type_scope list_scope]
+Arguments foo _%type_scope _%list_scope
 uncast = 
 fun (A : Type) (x : I A) => match x with
                             | x0 <: _ => x0
                             end
      : forall A : Type, I A -> A
 
-Argument scopes are [type_scope _]
+Arguments uncast _%type_scope
 foo' = if A 0 then true else false
      : bool
 f = 
@@ -82,7 +82,7 @@ lem2 =
 fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl
      : forall k : bool, k = k
 
-Argument scope is [bool_scope]
+Arguments lem2 _%bool_scope
 lem3 = 
 fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
      : forall k : nat * nat, k = k
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 3b65003c29..d65d2a8f55 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,8 +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 x, x0 are implicit
-Argument scopes are [nat_scope nat_scope _]
+Arguments d2 [x%nat_scope] [x0%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 af202ea01c..8ff571ae55 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -3,5 +3,5 @@ Last occurrence of "list'" must have "A" as 1st argument in
  "A -> list' A -> list' (A * A)%type".
 Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
 
-For foo: Argument scopes are [type_scope _]
-For Foo: Argument scopes are [type_scope _]
+Arguments foo _%type_scope
+Arguments Foo _%type_scope
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index c17c63e724..ce058a6d34 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,11 +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}
 
-For sig2: Argument A is implicit
-For exist2: Argument A is implicit
-For sig2: Argument scopes are [type_scope type_scope type_scope]
-For exist2: Argument scopes are [type_scope function_scope function_scope _ _
-              _]
+Arguments sig2 [A%type_scope] _%type_scope _%type_scope
+Arguments exist2 [A%type_scope] _%function_scope _%function_scope
 exists x : nat, x = x
      : Prop
 fun b : bool => if b then b else b
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index d32cf67e28..abada44da7 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -230,7 +230,7 @@ fun l : list nat => match l with
                     end
      : list nat -> list nat
 
-Argument scope is [list_scope]
+Arguments foo _%list_scope
 Notation
 "'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope
 (default interpretation)
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 8a6d94c732..2952b6d94b 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -15,8 +15,7 @@ swap =
 fun (A B : Type) '(x, y) => (y, x)
      : forall A B : Type, A * B -> B * A
 
-Arguments A, B are implicit and maximally inserted
-Argument scopes are [type_scope type_scope _]
+Arguments swap {A%type_scope} {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)
@@ -42,6 +41,6 @@ fun (pat : nat) '(x, y) => x + y = pat
 f = fun x : nat => x + x
      : nat -> nat
 
-Argument scope is [nat_scope]
+Arguments f _%nat_scope
 fun x : nat => x + x
      : nat -> nat
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index e788977fb7..7d0d81a3e8 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -1,36 +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
-Argument A is implicit
-Argument scopes are [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}
 
-For sigT: Argument A is implicit
-For existT: Argument A is implicit
-For sigT: Argument scopes are [type_scope type_scope]
-For existT: Argument scopes are [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
 
-For eq: Argument A is implicit and maximally inserted
-For eq_refl, when applied to no arguments:
-  Arguments A, x are implicit and maximally inserted
-For eq_refl, when applied to 1 argument:
-  Argument A is implicit
-For eq: Argument scopes are [type_scope _ _]
-For eq_refl: Argument scopes are [type_scope _]
+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
-When applied to no arguments:
-  Arguments A, x are implicit and maximally inserted
-When applied to 1 argument:
-  Argument A is implicit
-Argument scopes are [type_scope _]
+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
 
@@ -46,11 +34,11 @@ fix add (n m : nat) {struct n} : nat :=
   end
      : nat -> nat -> nat
 
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.add _%nat_scope _%nat_scope
 Nat.add : nat -> nat -> nat
 
 Nat.add is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.add _%nat_scope _%nat_scope
 Nat.add is transparent
 Expands to: Constant Coq.Init.Nat.add
 Nat.add : nat -> nat -> nat
@@ -58,17 +46,15 @@ Nat.add : nat -> nat -> nat
 plus_n_O : forall n : nat, n = n + 0
 
 plus_n_O is not universe polymorphic
-Argument scope is [nat_scope]
+Arguments plus_n_O _%nat_scope
 plus_n_O is opaque
 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
 
-For le_S: Argument m is implicit
-For le_S: Argument n is implicit and maximally inserted
-For le: Argument scopes are [nat_scope nat_scope]
-For le_n: Argument scope is [nat_scope]
-For le_S: Argument scopes are [nat_scope nat_scope _]
+Arguments le _%nat_scope _%nat_scope
+Arguments le_n _%nat_scope
+Arguments le_S {n%nat_scope} [m%nat_scope]
 comparison : Set
 
 comparison is not universe polymorphic
@@ -81,26 +67,21 @@ bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
-Argument x is implicit and maximally inserted
+Arguments bar {x}
 Expands to: Constant PrintInfos.bar
 *** [ bar : foo ]
 
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
-Argument x is implicit and maximally inserted
+Arguments bar {x}
 Module Coq.Init.Peano
 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
 
-For eq: Argument A is implicit and maximally inserted
-For eq_refl, when applied to no arguments:
-  Arguments A, x are implicit and maximally inserted
-For eq_refl, when applied to 1 argument:
-  Argument A is implicit and maximally inserted
-For eq: Argument scopes are [type_scope _ _]
-For eq_refl: Argument scopes are [type_scope _]
+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/StringSyntax.out b/test-suite/output/StringSyntax.out
index 9366113c0c..e9cf4282dc 100644
--- a/test-suite/output/StringSyntax.out
+++ b/test-suite/output/StringSyntax.out
@@ -433,7 +433,7 @@ end
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
+Arguments byte_rect _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope
 byte_rec = 
 fun P : byte -> Set => byte_rect P
      : forall P : byte -> Set,
@@ -607,7 +607,7 @@ fun P : byte -> Set => byte_rect P
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
+Arguments byte_rec _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope
 byte_ind = 
 fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") 
   (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") 
@@ -1043,7 +1043,7 @@ end
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
+Arguments byte_ind _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope
 "000"
      : byte
 "a"
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index d48d8b900f..298a0789c4 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -4,37 +4,36 @@ Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
 (* u |=  *)
 
 PWrap has primitive projections with eta conversion.
-For PWrap: Argument scope is [type_scope]
-For pwrap: Argument scopes are [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 |=  *)
 
-Argument scopes are [type_scope _]
+Arguments punwrap _%type_scope
 Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
 (* u |=  *)
 
-For RWrap: Argument scope is [type_scope]
-For rwrap: Argument scopes are [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 |=  *)
 
-Argument scopes are [type_scope _]
+Arguments runwrap _%type_scope
 Wrap@{u} = fun A : Type@{u} => A
      : Type@{u} -> Type@{u}
 (* u |=  *)
 
-Argument scope is [type_scope]
+Arguments Wrap _%type_scope
 wrap@{u} = 
 fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
      : forall A : Type@{u}, Wrap@{u} A -> A
 (* u |=  *)
 
-Arguments A, Wrap are implicit and maximally inserted
-Argument scopes are [type_scope _]
+Arguments wrap {A%type_scope} {Wrap}
 bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u *)
@@ -87,13 +86,13 @@ Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
 (* E |=  *)
 
 PWrap has primitive projections with eta conversion.
-For PWrap: Argument scope is [type_scope]
-For pwrap: Argument scopes are [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
-Argument scopes are [type_scope _]
+Arguments punwrap _%type_scope
 punwrap is transparent
 Expands to: Constant UnivBinders.punwrap
 The command has indeed failed with message:
@@ -118,7 +117,7 @@ Inductive insecind@{k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{k}
 (* k |=  *)
 
-For inseccstr: Argument scope is [type_scope]
+Arguments inseccstr _%type_scope
 insec@{u v} = Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
@@ -126,7 +125,7 @@ Inductive insecind@{u k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{u k}
 (* u k |=  *)
 
-For inseccstr: Argument scope is [type_scope]
+Arguments inseccstr _%type_scope
 insec2@{u} = Prop
      : Type@{Set+1}
 (* u |=  *)
@@ -148,24 +147,24 @@ Type@{UnivBinders.59} -> Type@{i}
 (* i UnivBinders.59 UnivBinders.60 |=  *)
 
 axfoo is universe polymorphic
-Argument scope is [type_scope]
+Arguments axfoo _%type_scope
 Expands to: Constant UnivBinders.axfoo
 axbar@{i UnivBinders.59 UnivBinders.60} :
 Type@{UnivBinders.60} -> Type@{i}
 (* i UnivBinders.59 UnivBinders.60 |=  *)
 
 axbar is universe polymorphic
-Argument scope is [type_scope]
+Arguments axbar _%type_scope
 Expands to: Constant UnivBinders.axbar
 axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
 
 axfoo' is not universe polymorphic
-Argument scope is [type_scope]
+Arguments axfoo' _%type_scope
 Expands to: Constant UnivBinders.axfoo'
 axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
 
 axbar' is not universe polymorphic
-Argument scope is [type_scope]
+Arguments axbar' _%type_scope
 Expands to: Constant UnivBinders.axbar'
 The command has indeed failed with message:
 When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block).