4 files changed, 51 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/5245.v b/test-suite/bugs/closed/5245.v
new file mode 100644
index 0000000000..77bf169e18
--- /dev/null
+++ b/test-suite/bugs/closed/5245.v
@@ -0,0 +1,18 @@
+Set Primitive Projections.
+
+Record foo := Foo {
+  foo_car : Type;
+  foo_rel : foo_car -> foo_car -> Prop
+}.
+Arguments foo_rel : simpl never.
+
+Definition foo_fun {A B} := Foo (A -> B) (fun f g => forall x, f x = g x).
+
+Goal @foo_rel foo_fun (fun x : nat => x) (fun x => x).
+Proof.
+intros x; exact eq_refl.
+Undo.
+progress hnf; intros; exact eq_refl.
+Undo.
+unfold foo_rel. intros x. exact eq_refl.
+Qed.
+\ No newline at end of file
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.