From e2da4d5758d0167cb621f2b57bb61708a2d6dbe4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 4 Dec 2012 23:26:21 +0000
Subject: Revised the strategy for automatic insertion of spaces when printing
 notations: - hopefully never 2 spaces when the user did not ask for - more
 systematic default insertion of spaces around symbols - e.g. have space
 before "[" if after a non-terminal - have spaces between consecutive
 terminals

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16019 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Notations.out  | 12 ++++++------
 test-suite/output/Notations2.out |  2 +-
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 6e59c36777..47eafe5537 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -8,17 +8,17 @@ fun e : nat * nat => proj1 e
 Identifier 'decomp' now a keyword
 decomp (true, true) as t, u in (t, u)
      : bool * bool
-!(0 = 0)
+! (0 = 0)
      : Prop
 forall n : nat, n = 0
      : Prop
-!(0 = 0)
+! (0 = 0)
      : Prop
-forall n : nat, #(n = n)
+forall n : nat, # (n = n)
      : Prop
-forall n n0 : nat, ##(n = n0)
+forall n n0 : nat, ## (n = n0)
      : Prop
-forall n n0 : nat, ###(n = n0)
+forall n n0 : nat, ### (n = n0)
      : Prop
 3 + 3
      : Z
@@ -42,7 +42,7 @@ Identifier 'ifn' now a keyword
 Identifier 'is' now a keyword
 fun x : nat => ifn x is succ n then n else 0
      : nat -> nat
-1-
+1 -
      : bool
 -4
      : Z
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index cf45025ea4..3639c6c3de 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
-- 
cgit v1.2.3