From b6e50de7f52a24aeeca0df0175fe5e5b327bfb90 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 28 Oct 2019 19:29:48 +0100
Subject: Fix output tests

---
 test-suite/output/InitSyntax.out | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

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

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