4 files changed, 50 insertions, 4 deletions
diff --git a/doc/changelog/04-tactics/14033-fix-14009.rst b/doc/changelog/04-tactics/14033-fix-14009.rst
new file mode 100644
index 0000000000..3b58e193cb
--- /dev/null
+++ b/doc/changelog/04-tactics/14033-fix-14009.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Properly expand projection parameters in hint discrimination
+  nets. (`#14033 <https://github.com/coq/coq/pull/14033>`_,
+  fixes `#9000 <https://github.com/coq/coq/issues/9000>`_,
+  `#14009 <https://github.com/coq/coq/issues/14009>`_,
+  by Pierre-Marie Pédrot).
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index af0ca22868..794d2bb94f 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -32,18 +32,25 @@ let compare_term_label t1 t2 = match t1, t2 with
 
 type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
 
-let decomp_pat =
+let decomp_pat p =
   let rec decrec acc = function
     | PApp (f,args) -> decrec (Array.to_list args @ acc) f
-    | PProj (p, c) -> (PRef (GlobRef.ConstRef (Projection.constant p)), c :: acc)
+    | PProj (p, c) ->
+      let hole = PMeta None in
+      let params = List.make (Projection.npars p) hole in
+      (PRef (GlobRef.ConstRef (Projection.constant p)), params @ c :: acc)
     | c -> (c,acc)
   in
-  decrec []
+  decrec [] p
 
 let decomp sigma t =
   let rec decrec acc c = match EConstr.kind sigma c with
     | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
-    | Proj (p, c) -> (mkConst (Projection.constant p), c :: acc)
+    | Proj (p, c) ->
+      (* Hack: fake evar to generate [Everything] in the functions below *)
+      let hole = mkEvar (Evar.unsafe_of_int (-1), []) in
+      let params = List.make (Projection.npars p) hole in
+      (mkConst (Projection.constant p), params @ c :: acc)
     | Cast (c1,_,_) -> decrec acc c1
     | _ -> (c,acc)
   in
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 _.