3 files changed, 37 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5749.v b/test-suite/bugs/closed/5749.v
new file mode 100644
index 0000000000..81bfe351c5
--- /dev/null
+++ b/test-suite/bugs/closed/5749.v
@@ -0,0 +1,18 @@
+(* Checking computation of free vars of a term for generalization *)
+
+Definition Decision := fun P : Prop => {P} + {~ P}.
+Class SetUnfold (P Q : Prop) : Prop := Build_SetUnfold { set_unfold : P <-> Q
+}.
+
+Section Filter_Help.
+
+  Context {A: Type}.
+  Context (fold_right : forall A B : Type, (B -> A -> A) -> A -> list B -> A).
+  Definition lType2 := (sigT (fun (P : A -> Prop) => forall a, Decision (P
+a))).
+  Definition test (X: lType2) := let (x, _) := X in x.
+
+  Global Instance foo `{fhl1 : list lType2} m Q:
+    SetUnfold (Q)
+              (fold_right _ _ (fun (s : lType2) => let (P, _) := s in and (P
+m)) (Q) (fhl1)).
diff --git a/test-suite/bugs/closed/5750.v b/test-suite/bugs/closed/5750.v
new file mode 100644
index 0000000000..6d0e21f5d0
--- /dev/null
+++ b/test-suite/bugs/closed/5750.v
@@ -0,0 +1,3 @@
+(* Check printability of the hole of the context *)
+Goal 0 = 0.
+match goal with |- context c [0] => idtac c end.
diff --git a/test-suite/bugs/closed/5755.v b/test-suite/bugs/closed/5755.v
new file mode 100644
index 0000000000..e07fdcf831
--- /dev/null
+++ b/test-suite/bugs/closed/5755.v
@@ -0,0 +1,16 @@
+(* Sections taking care of let-ins for inductive types *)
+
+Section Foo.
+
+Inductive foo (A : Type) (x : A) (y := x) (y : A) := Foo.
+
+End Foo.
+
+Section Foo2.
+
+Variable B : Type.
+Variable b : B.
+Let c := b.
+Inductive foo2 (A : Type) (x : A) (y := x) (y : A) := Foo2 : c=c -> foo2 A x y.
+
+End Foo2.