7 files changed, 52 insertions, 11 deletions
diff --git a/test-suite/output/CompactContexts.v b/test-suite/output/CompactContexts.v
index 07588d34f9..c409c0ee46 100644
--- a/test-suite/output/CompactContexts.v
+++ b/test-suite/output/CompactContexts.v
@@ -2,4 +2,4 @@ Set Printing Compact Contexts.
 
 Lemma f (hP1:True) (a:nat) (b:list nat) (h:forall (x:nat) , { y:nat | y > x}) (h2:True): False.
 Show.
-Abort.
-\ No newline at end of file
+Abort.
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 9d106d2dac..7bcd7b041c 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -133,3 +133,5 @@ fun (x : nat) (p : x = x) => match p with
                              | 1 => 1
                              end = p
      : forall x : nat, x = x -> Prop
+bar  0
+     : nat
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index b9985a594f..fe6c05c39e 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -291,3 +291,11 @@ Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p.
 Notation "1" := eq_refl.
 Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p.
 
+(* Check bug 5693 *)
+
+Module M.
+Definition A := 0.
+Definition bar (a b : nat) := plus a b.
+Notation "" := A (format "", only printing).
+Check (bar A 0).
+End M.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index a9ae74fd67..65efe228af 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -1,3 +1,5 @@
+{x : nat | x = 0} + {True /\ False} + {forall x : nat, x = 0}
+     : Set
 [<0, 2 >]
      : nat * nat * (nat * nat)
 [<0, 2 >]
@@ -109,9 +111,16 @@ fun x : ?A => x === x
      : forall x : ?A, x = x
 where
 ?A : [x : ?A |- Type] (x cannot be used)
-{0, 1}
+{{0, 1}}
      : nat * nat
-{0, 1, 2}
+{{0, 1, 2}}
      : nat * (nat * nat)
-{0, 1, 2, 3}
+{{0, 1, 2, 3}}
      : nat * (nat * (nat * nat))
+letpair x [1] = {0};
+return (1, 2, 3, 4)
+     : nat * nat * nat * nat
+{{ 1 | 1 // 1 }}
+     : nat
+!!! _ _ : nat, True
+     : (nat -> Prop) * ((nat -> Prop) * Prop)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index dee0f70f79..ea372ad1a3 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -1,4 +1,9 @@
 (**********************************************************************)
+(* Check precedence, spacing, etc. in printing with curly brackets    *)
+
+Check {x|x=0}+{True/\False}+{forall x, x=0}.
+
+(**********************************************************************)
 (* Check printing of notations with several instances of a recursive pattern *)
 (* Was wrong but I could not trigger a problem due to the collision between *)
 (* different instances of ".." *)
@@ -161,10 +166,27 @@ End Bug4765.
 Notation "x === x" := (eq_refl x) (only printing, at level 10).
 Check (fun x => eq_refl x).
 
-(**********************************************************************)
 (* Test recursive notations with the recursive pattern repeated on the right *)
 
-Notation "{ x , .. , y , z }" := (pair x .. (pair y z) ..).
-Check {0,1}.
-Check {0,1,2}.
-Check {0,1,2,3}.
+Notation "{{ x , .. , y , z }}" := (pair x .. (pair y z) ..).
+Check {{0,1}}.
+Check {{0,1,2}}.
+Check {{0,1,2,3}}.
+
+(* Test printing of #5608                                             *)
+
+Reserved Notation "'letpair' x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )"
+  (at level 200, format "'letpair'  x  [1]  =  { A } ; '//' 'return'  ( b0 ,  b1 ,  .. ,  b2 )").
+Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" :=
+  (let x:=a in ( .. (b0,b1) .., b2)).
+Check letpair x [1] = {0}; return (1,2,3,4).
+
+(* Test spacing in #5569 *)
+
+Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
+  (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
+Check 1+1+1.
+
+(* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
+Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
+Check !!! (x y:nat), True.
diff --git a/test-suite/output/SearchPattern.v b/test-suite/output/SearchPattern.v
index bde195a511..de9f48873a 100644
--- a/test-suite/output/SearchPattern.v
+++ b/test-suite/output/SearchPattern.v
@@ -33,4 +33,4 @@ Goal forall n (P:nat -> Prop), P n -> ~P n -> False.
   Search (P _) -"h'".       (* search hypothesis also for patterns *)
   Search (P _) -not.       (* search hypothesis also for patterns *)
 
-Abort.
-\ No newline at end of file
+Abort.
diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v
index 8ecd97aa56..91331a1de5 100644
--- a/test-suite/output/ltac_missing_args.v
+++ b/test-suite/output/ltac_missing_args.v
@@ -16,4 +16,4 @@ Goal True.
   Fail (fun _ => idtac).
   Fail rec True.
   Fail let rec tac x := tac in tac True.
-Abort.
-\ No newline at end of file
+Abort.