6 files changed, 63 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_3393.v b/test-suite/bugs/closed/bug_3393.v
index d2eb61e3e2..b0b573f5d5 100644
--- a/test-suite/bugs/closed/bug_3393.v
+++ b/test-suite/bugs/closed/bug_3393.v
@@ -109,6 +109,7 @@ Global Instance isisomorphism_compose' `{Funext}
        `{@IsIsomorphism (C -> D) F F' T}
 : @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation
   := @isisomorphism_compose (C -> D) _ _ T' _ _ T _.
+Arguments isisomorphism_compose' {H C D F' F''} T' {F} T {H0 H1}.
 Section lemmas.
   Context `{Funext}.
   Variable C : PreCategory.
diff --git a/test-suite/bugs/closed/bug_3422.v b/test-suite/bugs/closed/bug_3422.v
index 460ae8f110..1305104cdb 100644
--- a/test-suite/bugs/closed/bug_3422.v
+++ b/test-suite/bugs/closed/bug_3422.v
@@ -175,6 +175,7 @@ Global Instance isisomorphism_compose'
        `{@IsIsomorphism (C -> D) F F' T}
 : @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation
   := @isisomorphism_compose (C -> D) _ _ T' _ _ T _.
+Arguments isisomorphism_compose' {C D F' F''} T' {F} T {H H0}.
 
 Section lemmas.
   Local Open Scope natural_transformation_scope.
diff --git a/test-suite/bugs/closed/bug_5198.v b/test-suite/bugs/closed/bug_5198.v
index 5d4409f89b..4f24189d3f 100644
--- a/test-suite/bugs/closed/bug_5198.v
+++ b/test-suite/bugs/closed/bug_5198.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-boot" "-nois") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-nois") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 286 lines to
 27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines,
 then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from
diff --git a/test-suite/bugs/closed/bug_9313.v b/test-suite/bugs/closed/bug_9313.v
new file mode 100644
index 0000000000..0845e7732c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9313.v
@@ -0,0 +1,13 @@
+Set Implicit Arguments.
+Existing Class True.
+
+Instance foo1 (a : nat) {b : nat} (e : a = b) : True := I.
+Check foo1 (a := 3) (b := 4).
+
+Definition foo2 (a : nat) {b : nat} (e : a = b) : True := I.
+Check foo2 (a := 3) (b := 4).
+
+Instance foo3 (a : nat) {b : nat} (e : a = b) : True.
+exact I.
+Qed.
+Check foo3 (a := 3) (b := 4).
diff --git a/test-suite/bugs/closed/bug_9363.v b/test-suite/bugs/closed/bug_9363.v
new file mode 100644
index 0000000000..a3f6ad9fa2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9363.v
@@ -0,0 +1,17 @@
+(* Outside a section, Hypothesis, Variable, Axiom all obey implicit binders *)
+Hypothesis foo1 : forall {n : nat}, True.
+Variable foo1' : forall {n : nat}, True.
+Axiom foo1'' : forall {n : nat}, True.
+Check foo1 (n := 1).
+Check foo1' (n := 1).
+Check foo1'' (n := 1).
+
+Section bar.
+(* Inside a section, Hypothesis and Variable do not, but they should *)
+Hypothesis foo2 : forall {n : nat}, True.
+Variable foo2' : forall {n : nat}, True.
+Axiom foo2'' : forall {n : nat}, True.
+Check foo2 (n := 1).
+Check foo2' (n := 1).
+Check foo2'' (n := 1).
+End bar.
diff --git a/test-suite/bugs/closed/bug_9526.v b/test-suite/bugs/closed/bug_9526.v
new file mode 100644
index 0000000000..344d42083f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9526.v
@@ -0,0 +1,30 @@
+Primitive int := #int63_type.
+
+Module bad1.
+Polymorphic Inductive badcarry1 (A:Type) : Type :=
+| C0: A -> badcarry1 A
+| C1: A -> badcarry1 A.
+
+Fail Register badcarry1 as kernel.ind_carry.
+
+End bad1.
+
+Module bad2.
+
+Inductive badcarry2 (A:Set) : Set :=
+| C0: A -> badcarry2 A
+| C1: A -> badcarry2 A.
+
+Fail Register badcarry2 as kernel.ind_carry.
+
+End bad2.
+
+Module bad3.
+
+Inductive badcarry3 : Type -> Type  :=
+| C0: forall A, A -> badcarry3 A
+| C1: forall A, A -> badcarry3 A.
+
+Fail Register badcarry3 as kernel.ind_carry.
+
+End bad3.