diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 10 |
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) |