6 files changed, 59 insertions, 1 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_9166.v b/test-suite/bugs/closed/bug_9166.v
new file mode 100644
index 0000000000..8a7e9c37b0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9166.v
@@ -0,0 +1,9 @@
+Set Warnings "+deprecated".
+
+Notation bar := option (compat "8.7").
+
+Definition foo (x: nat) : nat :=
+  match x with
+  | 0 => 0
+  | S bar => bar
+  end.
diff --git a/test-suite/coqchk/inductive_functor_params.v b/test-suite/coqchk/inductive_functor_params.v
new file mode 100644
index 0000000000..f364a62818
--- /dev/null
+++ b/test-suite/coqchk/inductive_functor_params.v
@@ -0,0 +1,16 @@
+
+Module Type T.
+  Parameter foo : nat -> nat.
+End T.
+
+Module F (A:T).
+  Inductive ind (n:nat) : nat -> Prop :=
+  | C : (forall x, x < n -> ind (A.foo n) x) -> ind n n.
+End F.
+
+Module A. Definition foo (n:nat) := n. End A.
+
+Module M := F A.
+(* Note: M.ind could be seen as having 1 recursively uniform
+   parameter, but module substitution does not recognize it, so it is
+   treated as a non-uniform parameter. *)
diff --git a/test-suite/coqchk/inductive_functor_template.v b/test-suite/coqchk/inductive_functor_template.v
new file mode 100644
index 0000000000..bc5cd0fb68
--- /dev/null
+++ b/test-suite/coqchk/inductive_functor_template.v
@@ -0,0 +1,11 @@
+
+Module Type E. Parameter T : Type. End E.
+
+Module F (X:E).
+  #[universes(template)] Inductive foo := box : X.T -> foo.
+End F.
+
+Module ME. Definition T := nat. End ME.
+Module A := F ME.
+(* Note: A.foo could live in Set, and coqchk sees that (because of
+   template polymorphism implementation details) *)
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 97df40f882..844f96aaa1 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -51,7 +51,7 @@ Arguments pi _ _%F _%B.
 Check (forall w : r, pi w $ $ = tt).
 Fail Check (forall w : r, w $ $ = tt).
 Axiom w : r.
-Arguments w  _%F _%B : extra scopes.
+Arguments w  x%F y%B : extra scopes.
 Check (w $ $ = tt).
 Fail Arguments w  _%F _%B.