From a9fb1b03f50b7ac2d5a273b44f64ce49bc42db60 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 22 Jan 2019 10:39:50 +0100
Subject: [CS] recognize applied primitive projections as keys (fix #9375)

---
 pretyping/recordops.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'pretyping')

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]
-- 
cgit v1.2.3