From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 test-suite/output/Notations2.out | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

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

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index cf45025e..58ec1de5 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -1,6 +1,6 @@
 2 3
      : PAIR
-2[+]3
+2 [+] 3
      : nat
 forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x
      : Prop
@@ -10,7 +10,7 @@ end
      : nat
 let '(a, _, _) := (2, 3, 4) in a
      : nat
-exists myx (y : bool), myx = y
+exists myx y : bool, myx = y
      : Prop
 fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0
      : (nat -> nat -> Prop) -> nat -> Prop
@@ -24,7 +24,6 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d
      : Prop
 ∀ n p : nat, n + p = 0
      : Prop
-Identifier 'λ' now a keyword
 λ n p : nat, n + p = 0
      : nat -> nat -> Prop
 λ (A : Type) (n p : A), n = p
@@ -33,12 +32,11 @@ Identifier 'λ' now a keyword
      : Type -> Prop
 λ A : Type, ∀ n p : A, n = p
      : Type -> Prop
-Identifier 'let'' now a keyword
 let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
      : bool -> nat
 λ (f : nat -> nat) (x : nat), f(x) + S(x)
      : (nat -> nat) -> nat -> nat
-Notation plus2 n := (S (S n))
+Notation plus2 n := (S(S(n)))
 λ n : list(nat),
 match n with
 | nil => 2
-- 
cgit v1.2.3