1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_14009.v b/test-suite/bugs/closed/bug_14009.v
new file mode 100644
index 0000000000..bf86f5117e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_14009.v
@@ -0,0 +1,16 @@
+Class Bin {P:Type} (A B : P) := {}.
+
+Set Primitive Projections.
+
+Record test (n : nat) := { proj : Prop }.
+Axiom Bin_test : forall {t1 t2 : test O}, Bin (proj _ t1) (proj _ t2).
+
+Create HintDb db discriminated.
+#[local] Hint Resolve Bin_test : db.
+#[local] Hint Opaque proj : db.
+
+Goal forall t1 t2 : test O, Bin (proj O t1) (proj O t2).
+Proof.
+intros.
+solve [typeclasses eauto with db].
+Qed.