5 files changed, 113 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2881.v b/test-suite/bugs/closed/2881.v
new file mode 100644
index 0000000000..b4f09305b4
--- /dev/null
+++ b/test-suite/bugs/closed/2881.v
@@ -0,0 +1,7 @@
+(* About scoping of pattern variables in strict/non-strict mode *)
+
+Ltac eta_red := change (fun a => ?f0 a) with f0.
+Goal forall T1 T2 (f : T1 -> T2), (fun x => f x) = f.
+intros.
+eta_red.
+Abort.
diff --git a/test-suite/bugs/closed/5401.v b/test-suite/bugs/closed/5401.v
new file mode 100644
index 0000000000..95193b993b
--- /dev/null
+++ b/test-suite/bugs/closed/5401.v
@@ -0,0 +1,21 @@
+(* Testing printing of bound unnamed variables in pattern printer *)
+
+Module A.
+Parameter P : nat -> Type.
+Parameter v : forall m, P m.
+Parameter f : forall (P : nat -> Type), (forall a, P a) -> P 0.
+Class U (R : P 0) (m : forall x, P x) : Prop.
+Instance w : U (f _ (fun _ => v _)) v.
+Print HintDb typeclass_instances.
+End A.
+
+(* #5731 *)
+
+Module B.
+Axiom rel : Type -> Prop.
+Axiom arrow_rel : forall {A1}, A1 -> rel A1.
+Axiom forall_rel : forall E, (forall v1 : Type, E v1 -> rel v1) -> Prop.
+Axiom inl_rel: forall_rel _ (fun _ => arrow_rel).
+Hint Resolve inl_rel : foo.
+Print HintDb foo.
+End B.
diff --git a/test-suite/bugs/closed/5786.v b/test-suite/bugs/closed/5786.v
new file mode 100644
index 0000000000..20301ec4f5
--- /dev/null
+++ b/test-suite/bugs/closed/5786.v
@@ -0,0 +1,29 @@
+(* Printing all kinds of Ltac generic arguments *)
+
+Tactic Notation "myidtac" string(v) := idtac v.
+Goal True.
+myidtac "foo".
+Abort.
+
+Tactic Notation "myidtac2" ref(c) := idtac c.
+Goal True.
+myidtac2 True.
+Abort.
+
+Tactic Notation "myidtac3" preident(s) := idtac s.
+Goal True.
+myidtac3 foo.
+Abort.
+
+Tactic Notation "myidtac4" int_or_var(n) := idtac n.
+Goal True.
+myidtac4 3.
+Abort.
+
+Tactic Notation "myidtac5" ident(id) := idtac id.
+Goal True.
+myidtac5 foo.
+Abort.
+
+
+
diff --git a/test-suite/output/idtac.out b/test-suite/output/idtac.out
new file mode 100644
index 0000000000..3855f88a72
--- /dev/null
+++ b/test-suite/output/idtac.out
@@ -0,0 +1,11 @@
+"foo"
+True
+foo
+3
+foo
+2
+< True False Prop >
+< True False Prop >
+<  >
+<  >
+<< 1 2 3 >>
diff --git a/test-suite/output/idtac.v b/test-suite/output/idtac.v
new file mode 100644
index 0000000000..ac60ea9175
--- /dev/null
+++ b/test-suite/output/idtac.v
@@ -0,0 +1,45 @@
+(* Printing all kinds of Ltac generic arguments *)
+
+Tactic Notation "myidtac" string(v) := idtac v.
+Goal True.
+myidtac "foo".
+Abort.
+
+Tactic Notation "myidtac2" ref(c) := idtac c.
+Goal True.
+myidtac2 True.
+Abort.
+
+Tactic Notation "myidtac3" preident(s) := idtac s.
+Goal True.
+myidtac3 foo.
+Abort.
+
+Tactic Notation "myidtac4" int_or_var(n) := idtac n.
+Goal True.
+myidtac4 3.
+Abort.
+
+Tactic Notation "myidtac5" ident(id) := idtac id.
+Goal True.
+myidtac5 foo.
+Abort.
+
+(* Checking non focussing of idtac for integers *)
+Goal True/\True. split.
+all:let c:=numgoals in idtac c.
+Abort.
+
+(* Checking printing of lists and its focussing *)
+Tactic Notation "myidtac6" constr_list(l) := idtac "<" l ">".
+Goal True/\True. split.
+all:myidtac6 True False Prop.
+(* An empty list is focussing because of interp_genarg of a constr *)
+(* even if it is not focussing on printing *)
+all:myidtac6.
+Abort.
+
+Tactic Notation "myidtac7" int_list(l) := idtac "<<" l ">>".
+Goal True/\True. split.
+all:myidtac7 1 2 3.
+Abort.