Merge PR #10985: Print argument info as an Arguments command in About

Ack-by: Zimmi48
Ack-by: cpitclaudel
Reviewed-by: ejgallego

1 files changed, 2 insertions, 5 deletions

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