2 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_9300.v b/test-suite/bugs/closed/bug_9300.v
new file mode 100644
index 0000000000..a80f3233a3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9300.v
@@ -0,0 +1,6 @@
+Existing Class True.
+
+Instance foo {n : nat} (x := I) : forall {b : bool} (s : nat * nat), True. auto. Defined.
+
+Fail Check foo (n := 3) true (s := (4 , 5)).
+Check foo (n := 3) (b := true) (4 , 5).
diff --git a/test-suite/unit-tests/lib/pp_big_vect.ml b/test-suite/unit-tests/lib/pp_big_vect.ml
new file mode 100644
index 0000000000..e1cdd290e2
--- /dev/null
+++ b/test-suite/unit-tests/lib/pp_big_vect.ml
@@ -0,0 +1,14 @@
+open OUnit
+open Pp
+
+let pr_big_vect =
+  let n = "pr_big_vect" in
+  n >:: (fun () ->
+      let v = Array.make (1 lsl 20) () in
+      let pp = prvecti_with_sep spc (fun _ _ -> str"x") v in
+      let str = string_of_ppcmds pp in
+      ignore(str))
+
+let tests = [pr_big_vect]
+
+let () = Utest.run_tests __FILE__ (Utest.open_log_out_ch __FILE__) tests