4 files changed, 30 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_4509.v b/test-suite/bugs/closed/bug_4509.v
new file mode 100644
index 0000000000..ceae7c5fc3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4509.v
@@ -0,0 +1,11 @@
+(* Was solved at some time, suspectingly in PR #6328 *)
+
+Goal exists n, n > 1.
+Proof.
+  unshelve eexists. (*2 goals, as expected*)
+  Undo.
+  unshelve (eexists; instantiate (1:=ltac:(idtac))). (*only 1 goal*)
+  shelve.
+  Undo.
+  2:unshelve instantiate (1:=_).
+Abort.
diff --git a/test-suite/bugs/closed/bug_6202.v b/test-suite/bugs/closed/bug_6202.v
new file mode 100644
index 0000000000..899260f59a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_6202.v
@@ -0,0 +1,11 @@
+(* This was fixed at some time, suspectingly in PR #6328 *)
+
+Inductive foo := F (a : forall var : Type -> Type, unit -> var unit) (_ : a = a).
+Goal foo.
+  eexists (fun var => fun u : unit => ltac:(clear u)).
+  shelve.
+  Unshelve.
+  all:[ > | ].
+  shelve.
+  Fail Grab Existential Variables.
+Abort.
diff --git a/test-suite/bugs/closed/bug_8819.v b/test-suite/bugs/closed/bug_8819.v
new file mode 100644
index 0000000000..a4cb9dcd14
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8819.v
@@ -0,0 +1,2 @@
+Theorem foo (_ : nat) (H : bool) : bool.
+Proof. exact H. Qed.
diff --git a/test-suite/bugs/closed/bug_9229.v b/test-suite/bugs/closed/bug_9229.v
new file mode 100644
index 0000000000..7514741af4
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9229.v
@@ -0,0 +1,6 @@
+(* There was a problem of freshness with Infix choice of vars *)
+
+(* In particular, x and y were special... *)
+
+Infix "#" := (fun x y => x + y) (at level 50, left associativity).
+Check (3 # 5).