Merge branch 'v8.5'

1 files changed, 9 insertions, 1 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 229508ea3..551632962 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -794,7 +794,15 @@ let rec subterm_specif renv stack t =
     | Proj (p, c) -> 
       let subt = subterm_specif renv stack c in
 	(match subt with
-	| Subterm (s, wf) -> Subterm (Strict, wf)
+	| Subterm (s, wf) ->
+	   (* We take the subterm specs of the constructor of the record *)
+	   let wf_args = (dest_subterms wf).(0) in
+	   (* We extract the tree of the projected argument *)
+	   let kn = Projection.constant p in
+	   let cb = lookup_constant kn renv.env in
+	   let pb = Option.get cb.const_proj in
+	   let n = pb.proj_arg in
+	   Subterm (Strict, List.nth wf_args n)
 	| Dead_code -> Dead_code
 	| Not_subterm -> Not_subterm)