diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 6975544acf..58909ce012 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -814,6 +814,13 @@ let rec subterm_specif renv stack t = (* Metas and evars are considered OK *) | (Meta _|Evar _) -> Dead_code + | Proj (p, c) -> + let subt = subterm_specif renv stack c in + (match subt with + | Subterm (s, wf) -> Subterm (Strict, wf) + | Dead_code -> Dead_code + | Not_subterm -> Not_subterm) + (* Other terms are not subterms *) | _ -> Not_subterm |