[test-suite] Fix output tests due to merge problems.

2 files changed, 19 insertions, 19 deletions

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index a36ab2e0dc..e121b5e86c 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -81,18 +81,18 @@ fun x : nat => [x]
      : nat -> nat
 ∀ x : nat, x = x
      : Prop
-File "stdin", line 222, characters 0-160:
+File "stdin", line 219, characters 0-160:
 Warning: Notation "∀ _ .. _ , _" was already defined with a different format
 in scope type_scope. [notation-incompatible-format,parsing]
 ∀x : nat,x = x
      : Prop
-File "stdin", line 235, characters 0-60:
+File "stdin", line 232, characters 0-60:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 239, characters 0-64:
+File "stdin", line 236, characters 0-64:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 244, characters 0-62:
+File "stdin", line 241, characters 0-62:
 Warning: Lonely notation "_ %%%% _" was already defined with a different
 format. [notation-incompatible-format,parsing]
 3  %%  4
@@ -101,9 +101,9 @@ format. [notation-incompatible-format,parsing]
      : nat
 3   %%   4
      : nat
-File "stdin", line 272, characters 0-61:
+File "stdin", line 269, characters 0-61:
 Warning: The format modifier is irrelevant for only parsing rules.
 [irrelevant-format-only-parsing,parsing]
-File "stdin", line 276, characters 0-63:
+File "stdin", line 273, characters 0-63:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing]
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 83dd2f40fb..c5b4d6f291 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -6,13 +6,13 @@ where
 ?B : [ |- Type]
 p 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-p 0 0 (B:=bool)
+p 0 0
      : forall b : bool, 0 = 0 /\ b = b
-p 0 0 (B:=bool)
+p 0 0
      : forall b : bool, 0 = 0 /\ b = b
-p (A:=nat)
+p
      : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
-p (A:=nat)
+p
      : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
 @p nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
@@ -44,16 +44,16 @@ p
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
 f x true
      : 0 = 0 /\ true = true
-f x (B:=bool)
+f x
      : forall b : bool, 0 = 0 /\ b = b
-f x (B:=bool)
+f x
      : forall b : bool, 0 = 0 /\ b = b
 @f nat
      : forall a1 a2 : nat,
        T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
-f (a1:=0) (a2:=0)
+f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
-f (a1:=0) (a2:=0)
+f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
 @f
      : forall (A : Type) (a1 a2 : A),
@@ -62,16 +62,16 @@ f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
 x.(f) true
      : 0 = 0 /\ true = true
-x.(f) (B:=bool)
+x.(f)
      : forall b : bool, 0 = 0 /\ b = b
-x.(f) (B:=bool)
+x.(f)
      : forall b : bool, 0 = 0 /\ b = b
 @f nat
      : forall a1 a2 : nat,
        T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
-f (a1:=0) (a2:=0)
+f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
-f (a1:=0) (a2:=0)
+f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
 @f
      : forall (A : Type) (a1 a2 : A),
@@ -218,7 +218,7 @@ p 0 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0 (B:=bool)
+p 0 0
      : forall b : bool, 0 = 0 /\ b = b
 p 0 0 true
      : 0 = 0 /\ true = true