diff options
| author | herbelin | 2012-12-04 23:26:21 +0000 |
|---|---|---|
| committer | herbelin | 2012-12-04 23:26:21 +0000 |
| commit | e2da4d5758d0167cb621f2b57bb61708a2d6dbe4 (patch) | |
| tree | 3e25d69ffb034bc386b4f737be723ec6f141628d /test-suite/output | |
| parent | a05c335c2d38a5cf08bc0fda76d69a13e0ead040 (diff) | |
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
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Notations.out | 12 | ||||
| -rw-r--r-- | test-suite/output/Notations2.out | 2 |
2 files changed, 7 insertions, 7 deletions
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 |