3 files changed, 37 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_8364.v b/test-suite/bugs/closed/bug_8364.v
new file mode 100644
index 0000000000..10f955b41f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8364.v
@@ -0,0 +1,17 @@
+Unset Primitive Projections.
+
+Record Box (A:Type) := box { unbox : A }.
+Arguments box {_} _. Arguments unbox {_} _.
+
+Definition map {A B} (f:A -> B) x :=
+  match x with box x => box (f x) end.
+
+Definition tuple (l : Box Type) : Type :=
+  match l with
+  | box x => x
+  end.
+
+Fail Inductive stack : Type -> Type :=
+| Stack T foos :
+  tuple (map stack foos) ->
+  stack T.
diff --git a/test-suite/bugs/closed/bug_9014.v b/test-suite/bugs/closed/bug_9014.v
new file mode 100644
index 0000000000..c1fdd04a65
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9014.v
@@ -0,0 +1,19 @@
+(* A type, not a class *)
+Variant T := mkT.
+
+(* In records, :> declares a coercion *)
+Record R := { t_of_r :> T }.
+Check forall r : R, r = r :> T.
+
+(* A class *)
+Class A := { p : Prop }.
+(* A sub-class *)
+Class B := { a_of_b :> A ; t_of_b :> T }.
+(* The sub-instance is automatically inferred due to :> for a_of_b *)
+Check forall b : B, p.
+(* No coercion is introduced by :> in t_of_b *)
+Fail Check forall b : B, b = b :> T.
+
+(* Using :> when the RHS is not a class produces a “not-a-class” warning. *)
+Set Warnings "+not-a-class".
+Fail Class B' := { a_of_b' :> A ; t_of_b' :> T }.
diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v
index d2116d2183..95daa1bb0c 100644
--- a/test-suite/modules/Nat.v
+++ b/test-suite/modules/Nat.v
@@ -2,7 +2,7 @@ Definition T := nat.
 
 Definition le := le.
 
-Hint Unfold le.
+Hint Unfold le : core.
 
 Lemma le_refl : forall n : nat, le n n.
   auto.