7 files changed, 88 insertions, 12 deletions
diff --git a/test-suite/bugs/closed/5469.v b/test-suite/bugs/closed/5469.v
deleted file mode 100644
index fce671c754..0000000000
--- a/test-suite/bugs/closed/5469.v
+++ /dev/null
@@ -1,3 +0,0 @@
-(* Some problems with the special treatment of curly braces *)
-
-Reserved Notation "'a' { x }" (at level 0, format "'a' { x }").
diff --git a/test-suite/bugs/closed/5608.v b/test-suite/bugs/closed/5608.v
new file mode 100644
index 0000000000..f02eae69c2
--- /dev/null
+++ b/test-suite/bugs/closed/5608.v
@@ -0,0 +1,33 @@
+Reserved Notation "'slet' x .. y := A 'in' b"
+  (at level 200, x binder, y binder, b at level 200, format "'slet'  x .. y  :=  A  'in' '//' b").
+Reserved Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )"
+  (at level 200, format "T  x [1]  =  { A } ; '//' 'return'  ( b0 ,  b1 ,  .. ,  b2 )").
+
+Delimit Scope ctype_scope with ctype.
+Local Open Scope ctype_scope.
+Delimit Scope expr_scope with expr.
+Inductive base_type := TZ | TWord (logsz : nat).
+Inductive flat_type := Tbase (T : base_type) | Prod (A B : flat_type).
+Context {var : base_type -> Type}.
+Fixpoint interp_flat_type (interp_base_type : base_type -> Type) (t : 
+flat_type) :=
+  match t with
+  | Tbase t => interp_base_type t
+  | Prod x y => prod (interp_flat_type interp_base_type x) (interp_flat_type 
+interp_base_type y)
+  end.
+Inductive exprf : flat_type -> Type :=
+| Var {t} (v : var t) : exprf (Tbase t)
+| LetIn {tx} (ex : exprf tx) {tC} (eC : interp_flat_type var tx -> exprf tC) : 
+exprf tC
+| Pair {tx} (ex : exprf tx) {ty} (ey : exprf ty) : exprf (Prod tx ty).
+Global Arguments Var {_} _.
+Global Arguments LetIn {_} _ {_} _.
+Global Arguments Pair {_} _ {_} _.
+Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" := (LetIn (tx:=T) A 
+(fun x => Pair .. (Pair b0%expr b1%expr) .. b2%expr)) : expr_scope.
+Definition foo :=
+  (fun x3 =>
+     (LetIn (Var x3) (fun x18 : var TZ
+                      => (Pair (Var x18) (Var x18))))).
+Print foo.
diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v
index 39a7103d1b..40abb215e9 100644
--- a/test-suite/bugs/closed/HoTT_coq_032.v
+++ b/test-suite/bugs/closed/HoTT_coq_032.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; coq-prog-args: ("-xml") -*- *)
 Set Implicit Arguments.
 Generalizable All Variables.
 Set Asymmetric Patterns.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index a9ae74fd67..e5dbfcb4be 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,14 @@ 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
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index dee0f70f79..b1015137d6 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,23 @@ 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.
diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v
index 0ed5b524f3..4e36dec15b 100644
--- a/test-suite/success/forward.v
+++ b/test-suite/success/forward.v
@@ -16,3 +16,14 @@ eremember (S (S ?[x])).
 instantiate (x:=0).
 reflexivity.
 Qed.
+
+(* Don't know if it is good or not but the compatibility tells that
+   the asserted goal to prove is subject to beta-iota but not the
+   asserted hypothesis *)
+
+Goal True.
+assert ((fun x => x) False).
+Fail match goal with |- (?f ?a) => idtac end. (* should be beta-iota reduced *)
+2:match goal with _: (?f ?a) |- _ => idtac end. (* should not be beta-iota reduced *)
+Abort.
+
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 1d35f1ef6c..29e373eaa5 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -337,3 +337,14 @@ Goal True.
 evar (0=0).
 Abort.
 
+(* Test location of hypothesis in "symmetry in H". This was broken in
+   8.6 where H, when the oldest hyp, was moved at the place of most
+   recent hypothesis *)
+
+Goal 0=1 -> True -> True.
+intros H H0.
+symmetry in H.
+(* H should be the first hypothesis *)
+match goal with h:_ |- _ => assert (h=h) end. (* h should be H0 *)
+exact (eq_refl H0).
+Abort.