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 | |
| 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')
| -rw-r--r-- | kernel/indtypes.ml | 4 | ||||
| -rw-r--r-- | kernel/inductive.ml | 7 |
2 files changed, 9 insertions, 2 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 2e9a81d98f..4feec40e8f 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -686,14 +686,14 @@ let compute_projections ((kn, _ as ind), u as indsp) n nparamargs params in let projections (na, b, t) (i, j, kns, pbs, subst) = match b with - | Some c -> (i, j+1, kns, pbs, c :: subst) + | Some c -> (i, j+1, kns, pbs, substl subst c :: subst) | None -> match na with | Name id -> let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in let ty = substl subst (liftn 1 j t) in let term = mkProj (kn, mkRel 1) in - let compat = compat_body ty i in + let compat = compat_body ty (j - 1) in let etab = it_mkLambda_or_LetIn (mkLambda (x, rp, term)) params in let etat = it_mkProd_or_LetIn (mkProd (x, rp, ty)) params in let body = { proj_ind = fst ind; proj_npars = nparamargs; 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 |