From aa55f7b0bedec1ee5c416dbaa9b1478537b76e72 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 20 Nov 2019 16:46:03 +0100
Subject: Combine similar arguments when printing Arguments command

"similar" means sharing a scope or implicit status.
---
 test-suite/output/InitSyntax.out | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite/output/InitSyntax.out')

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
-- 
cgit v1.2.3