6 files changed, 29 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2810.v b/test-suite/bugs/closed/2810.v
new file mode 100644
index 000000000..9e33e4916
--- /dev/null
+++ b/test-suite/bugs/closed/2810.v
@@ -0,0 +1,9 @@
+Section foo.
+  Variable A : Type.
+  Let B := A.
+
+  Hint Unfold B.
+
+  Goal False.
+    clear B. autounfold with core.
+End foo.
diff --git a/test-suite/bugs/closed/2828.v b/test-suite/bugs/closed/2828.v
new file mode 100644
index 000000000..0b8abace2
--- /dev/null
+++ b/test-suite/bugs/closed/2828.v
@@ -0,0 +1,4 @@
+Parameter A B : Type.
+Coercion POL (p : prod A B) := fst p.
+Goal forall x : prod A B, A.
+  intro x. Fail exact x.
diff --git a/test-suite/bugs/closed/2850.v b/test-suite/bugs/closed/2850.v
new file mode 100644
index 000000000..64a93aeb0
--- /dev/null
+++ b/test-suite/bugs/closed/2850.v
@@ -0,0 +1,2 @@
+Definition id {A} (x : A) := x.
+Fail Compute id.
diff --git a/test-suite/bugs/closed/2854.v b/test-suite/bugs/closed/2854.v
new file mode 100644
index 000000000..14aee17ff
--- /dev/null
+++ b/test-suite/bugs/closed/2854.v
@@ -0,0 +1,7 @@
+Section foo.
+  Let foo := Type.
+  Definition bar : foo -> foo := @id _.
+  Goal False.
+    subst foo.
+    Fail pose bar as f.
+    (* simpl in f. *)
diff --git a/test-suite/bugs/closed/2920.v b/test-suite/bugs/closed/2920.v
new file mode 100644
index 000000000..13548b9e4
--- /dev/null
+++ b/test-suite/bugs/closed/2920.v
@@ -0,0 +1,2 @@
+Fail Definition my_f_equal {A B : Type} (f : A -> B) (a a' : A) (p : a = a') : f a = f a' :=
+  eq_ind _ _ (fun a' => f a = f a') _ _ p.
diff --git a/test-suite/bugs/closed/2945.v b/test-suite/bugs/closed/2945.v
new file mode 100644
index 000000000..59b57c07b
--- /dev/null
+++ b/test-suite/bugs/closed/2945.v
@@ -0,0 +1,5 @@
+Notation "f1 =1 f2 :> A" := (f1 = (f2 : A))
+  (at level 70, f2 at next level, A at level 90) : fun_scope.
+
+Notation "e :? pf" := (eq_rect _ (fun X : _ => X) e _ pf)
+  (no associativity, at level 90).