diff options
| author | Matthieu Sozeau | 2014-09-10 12:56:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-10 13:01:24 +0200 |
| commit | 6624459e492164b3d189e3518864379ff985bf8c (patch) | |
| tree | 9fc004c5f25927f671667d0cf5475061b306e1f0 /kernel/inductive.ml | |
| parent | c2fa953889cf7bcef9c369d175e156855ac0be2e (diff) | |
Fix generation of inductive elimination principle for primitive records.
Let r.(p) be a strict subterm of r during the guardness check.
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 |