Merge PR #14033: Properly expand projection parameters in Btermdn.

Reviewed-by: mattam82

2 files changed, 33 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.
diff --git a/test-suite/bugs/closed/bug_9000.v b/test-suite/bugs/closed/bug_9000.v
new file mode 100644
index 0000000000..e239c8b1fe
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9000.v
@@ -0,0 +1,17 @@
+Set Primitive Projections.
+Class type (t : Type) : Type :=
+  { bar : t -> Prop  }.
+
+Instance type_nat : type nat :=
+  { bar := fun _ => True }.
+
+Definition foo_bar {n : nat} : bar n := I.
+
+#[local] Hint Resolve (@foo_bar) : typeclass_instances.
+#[local] Hint Resolve I : typeclass_instances.
+Check ltac:(typeclasses eauto with nocore typeclass_instances) : True.
+Check ltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _.
+Existing Class bar.
+Check ltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _.
+#[local] Hint Resolve (@foo_bar) : foo.
+Check ltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _.