Fixing multiple printing bugs with "Notation f x := ..."

- Missing space and bad constr level in "About f"
- Display of arguments missing when used as a pattern notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13966 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 17 insertions, 0 deletions

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 444d6b0910..5a4a72303c 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -27,3 +27,13 @@ let' f (x y 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))
+λ n : list(nat),
+match n with
+| nil => 2
+| 0 :: _ => 2
+| list1 => 0
+| 1 :: _ :: _ => 2
+| plus2 _ :: _ => 2
+end
+     : list(nat) -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index e7b0b97546..635b254166 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -60,6 +60,13 @@ Check let' f x y z (a:bool) := x+y+z+1 in f 0 1 2.
 Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
 Check fun f x => f x + S x.
 
+Open Scope list_scope.
+Notation list1 := (1::nil)%list.
+Notation plus2 n := (S (S n)).
+(* plus2 was not correctly printed in the two following tests in 8.3pl1 *)
+Print plus2.
+Check fun n => match n with list1 => 0 | _ => 2 end.
+
 (* This one is not fully satisfactory because binders in the same type
    are re-factorized and parentheses are needed even for atomic binder