8 files changed, 54 insertions, 5 deletions
diff --git a/test-suite/bugs/closed/bug_2830.v b/test-suite/bugs/closed/bug_2830.v
index 801c61b132..a321bb324e 100644
--- a/test-suite/bugs/closed/bug_2830.v
+++ b/test-suite/bugs/closed/bug_2830.v
@@ -194,14 +194,17 @@ Instance skel_equiv A : Equivalence (@skel A).
 Admitted.
 
 Import FunctionalExtensionality.
-Instance set_cat : Category Type (fun A B => A -> B) := {
+
+Instance set_cat : Category Type (fun A B => A -> B).
+refine {|
   id := fun A => fun x => x
   ; comp c b a f g := fun x => f (g x)
   ; eqv := fun A B => @skel (A -> B)
-}.
+|}.
 intros. compute. symmetry. apply eta_expansion.
 intros. compute. symmetry. apply eta_expansion.
-intros. compute. reflexivity. Defined.
+intros. compute. reflexivity.
+Defined.
 
 (* The [list] type constructor is a Functor. *)
 
diff --git a/test-suite/bugs/closed/bug_3495.v b/test-suite/bugs/closed/bug_3495.v
index 7b0883f910..47db64a096 100644
--- a/test-suite/bugs/closed/bug_3495.v
+++ b/test-suite/bugs/closed/bug_3495.v
@@ -1,7 +1,7 @@
 Require Import RelationClasses.
 
 Axiom R : Prop -> Prop -> Prop.
-Declare Instance : Reflexive R.
+Declare Instance R_refl : Reflexive R.
 
 Class bar := { x : False }.
 Record foo := { a : Prop ; b : bar }.
diff --git a/test-suite/bugs/closed/bug_4498.v b/test-suite/bugs/closed/bug_4498.v
index 379e46b3e3..9b3210860c 100644
--- a/test-suite/bugs/closed/bug_4498.v
+++ b/test-suite/bugs/closed/bug_4498.v
@@ -19,6 +19,6 @@ Class Category := {
 
 Require Export Coq.Setoids.Setoid.
 
-Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with
+Add Parametric Morphism `{Category} {A B C} : (@compose _ A B C) with
   signature equiv ==> equiv ==> equiv as compose_mor.
 Proof. apply comp_respects. Qed.
diff --git a/test-suite/bugs/closed/bug_9329.v b/test-suite/bugs/closed/bug_9329.v
new file mode 100644
index 0000000000..c0322dec40
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9329.v
@@ -0,0 +1,12 @@
+(* Declare empty levels in the same order they are computed *)
+
+Notation "< a ; b ; c >1" :=
+  (sum a (sum b c)) (at level 18, a at level 19, b at level 20, c at level 21).
+Notation "< a ; b ; c >2" :=
+  (sum a (sum b c)) (at level 28, a at level 29, c at level 32, b at level 31).
+Notation "< a ; b ; c >3" :=
+  (sum a (sum b c)) (at level 38, c at level 42, a at level 39, b at level 41).
+Notation "< a ; b ; c >4" :=
+  (sum a (sum b c)) (at level 48, c at level 52, b at level 51, a at level 49).
+Notation "< a ; b >" :=
+  (sum a b) (at level 61, a at level 63, b at level 62).
diff --git a/test-suite/bugs/closed/bug_9375.v b/test-suite/bugs/closed/bug_9375.v
new file mode 100644
index 0000000000..a2bfbafe06
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9375.v
@@ -0,0 +1,16 @@
+Set Primitive Projections.
+
+Record toto : Type := Toto {
+  toto1 : Type;
+  toto2 : toto1 -> Type
+}.
+
+Record tata := Tata {
+  tata1 : Type
+}.
+
+Canonical Structure tata_toto (x : toto) X :=
+  Tata (toto2 x X).
+
+Check fun (T : toto) (t : toto1 T) =>
+   (eq_refl _ : @tata1 _ = @toto2 _ t).
diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v
index 78b2aa69b9..9d83743b2a 100644
--- a/test-suite/bugs/opened/bug_3890.v
+++ b/test-suite/bugs/opened/bug_3890.v
@@ -3,7 +3,9 @@ Set Nested Proofs Allowed.
 Class Foo.
 Class Bar := b : Type.
 
+Set Refine Instance Mode.
 Instance foo : Foo := _.
+Unset Refine Instance Mode.
 (* 1 subgoals, subgoal 1 (ID 4)
 
   ============================
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 400479ae85..9086621344 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -198,7 +198,9 @@ Module UniqueInstances.
       for it. *)
   Set Typeclasses Unique Instances.
   Class Eq (A : Type) : Set.
+    Set Refine Instance Mode.
     Instance eqa : Eq nat := _. constructor. Qed.
+    Unset Refine Instance Mode.
     Instance eqb : Eq nat := {}.
     Class Foo (A : Type) (e : Eq A) : Set.
     Instance fooa : Foo _ eqa := {}.
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