Merge PR #9377: [CS] recognize applied primitive projections as keys (fix #9375)

Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: mattam82
Ack-by: ppedrot

2 files changed, 24 insertions, 1 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 6e3b19ae61..f58cce41cc 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -202,7 +202,14 @@ let cs_pattern_of_constr env t =
       App (f,vargs) ->
 	begin
 	  try Const_cs (global_of_constr f) , None, Array.to_list vargs
-          with e when CErrors.noncritical e -> raise Not_found
+          with
+          | Not_found when isProj f ->
+              let p, c = destProj f in
+              let { Environ.uj_type = ty } = Typeops.infer env c in
+              let _, params = Inductive.find_rectype env ty in
+              Const_cs (ConstRef (Projection.constant p)), None,
+              params @ [c] @ Array.to_list vargs
+          | e when CErrors.noncritical e -> raise Not_found
 	end
     | Rel n -> Default_cs, Some n, []
     | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
diff --git a/test-suite/bugs/closed/bug_9375.v b/test-suite/bugs/closed/bug_9375.v
new file mode 100644
index 0000000000..a2bfbafe06
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9375.v
@@ -0,0 +1,16 @@
+Set Primitive Projections.
+
+Record toto : Type := Toto {
+  toto1 : Type;
+  toto2 : toto1 -> Type
+}.
+
+Record tata := Tata {
+  tata1 : Type
+}.
+
+Canonical Structure tata_toto (x : toto) X :=
+  Tata (toto2 x X).
+
+Check fun (T : toto) (t : toto1 T) =>
+   (eq_refl _ : @tata1 _ = @toto2 _ t).