This fix is probably not enough to justify that there are no problems with

primitive projections and prop. ext. or univalence, but at least it prevents
known proofs of false (see discussion on #4588).

1 files changed, 9 insertions, 1 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 80dc69042..fbe0920bc 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -814,7 +814,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)