7 files changed, 67 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_10025.v b/test-suite/bugs/closed/bug_10025.v
new file mode 100644
index 0000000000..1effc771b0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10025.v
@@ -0,0 +1,39 @@
+Require Import Program.
+
+Axiom I : Type.
+
+Inductive S : Type := NT : I -> S.
+
+Axiom F : S -> Type.
+
+Axiom G : forall (s : S), F s -> Type.
+
+Section S.
+
+Variable init : I.
+Variable my_s : F (NT init).
+
+Inductive foo : forall (s: S) (hole_sem: F s), Type :=
+| Foo : foo (NT init) my_s.
+
+Goal forall
+  (n : I) (s : F (NT n)) (ptz : foo (NT n) s) (pt : G (NT n) s) (x : unit),
+match
+  match x with tt => tt end
+with
+| tt =>
+    match
+      match ptz in foo x s return (forall _ : G x s, unit) with
+      | Foo => fun _ : G (NT init) my_s => tt
+      end pt
+    with
+    | tt => False
+    end
+end.
+Proof.
+dependent destruction ptz.
+(* Check well-typedness of goal *)
+match goal with [ |- ?P ] => let t := type of P in idtac end.
+Abort.
+
+End S.
diff --git a/test-suite/bugs/closed/bug_10026.v b/test-suite/bugs/closed/bug_10026.v
new file mode 100644
index 0000000000..0d3142d0f2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10026.v
@@ -0,0 +1,3 @@
+Require Import Coq.Lists.List.
+Set Debug RAKAM.
+Check fun _ => fold_right (fun A B => prod A B) unit _.
diff --git a/test-suite/bugs/closed/bug_10031.v b/test-suite/bugs/closed/bug_10031.v
new file mode 100644
index 0000000000..15b53de00d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10031.v
@@ -0,0 +1,9 @@
+Require Import Int63 ZArith.
+
+Open Scope int63_scope.
+
+Goal False.
+cut (let (q, r) := (0, 0) in ([|q|], [|r|]) = (9223372036854775808%Z, 0%Z));
+  [discriminate| ].
+Fail (change (0, 0) with (diveucl_21 1 0 1); apply diveucl_21_spec).
+Abort.
diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/closed/bug_3754.v
index 18820b1a4c..7031cbf132 100644
--- a/test-suite/bugs/opened/bug_3754.v
+++ b/test-suite/bugs/closed/bug_3754.v
@@ -281,5 +281,7 @@ Defined.
                                  (factor2 fact)).
       rewrite <- ap_p_pp; rewrite_moveL_Mp_p.
       Set Debug Tactic Unification.
-      Fail rewrite (concat_Ap ff2).
+      rewrite (concat_Ap ff2).
     Abort.
+
+End Factorization.
diff --git a/test-suite/bugs/closed/bug_5752.v b/test-suite/bugs/closed/bug_5752.v
new file mode 100644
index 0000000000..b4218d66df
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5752.v
@@ -0,0 +1,8 @@
+Class C (A : Type) := c : A.
+
+Hint Mode C ! : typeclass_instances.
+
+Goal forall f : (forall A, C A -> C (list A)), True.
+intros.
+  Check c. (* Loops if modes are ignored. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_9344.v b/test-suite/bugs/closed/bug_9344.v
new file mode 100644
index 0000000000..0d44c9721a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9344.v
@@ -0,0 +1,2 @@
+Compute _ I.
+Eval native_compute in _ I.
diff --git a/test-suite/bugs/closed/bug_9348.v b/test-suite/bugs/closed/bug_9348.v
new file mode 100644
index 0000000000..a4673b5ffc
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9348.v
@@ -0,0 +1,3 @@
+Set Primitive Projections.
+Record r {A} := R {f : A -> A}.
+Compute f _ I.