From 120053a50f87bd53398eedc887fa5e979f56f112 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 4 Mar 2016 18:17:56 +0100 Subject: 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). --- kernel/inductive.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'kernel/inductive.ml') 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) -- cgit v1.2.3