diff options
| author | herbelin | 2000-09-15 16:44:52 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-15 16:44:52 +0000 |
| commit | f7da904e8702bd144f25fa3a80307a994a39f1d6 (patch) | |
| tree | 57dffffc91f349ebc974b745d277c70d4830b83f /kernel/indtypes.ml | |
| parent | ccc5d85d36898c283a41230d0269b6ce701930cd (diff) | |
On laisse les LetIn dans les types des constructeurs et des éliminations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@612 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index ee58603117..c29d4385d5 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -272,9 +272,10 @@ let listrec_mconstr env ntypes nparams i indlc = | IsLetIn (na,b,t,d) -> assert (largs = []); if not (noccur_between n ntypes b & noccur_between n ntypes t) then - raise (IllFormedInd (LocalNonPos n)); - let recarg = check_pos n b in - check_constr_rec lrec (n+1) d + check_constr_rec lrec n (subst1 b d) + else + let recarg = check_pos n b in + check_constr_rec lrec (n+1) d | hd -> if check_head then @@ -320,8 +321,9 @@ let cci_inductive env env_ar kind nparams finite inds cst = Some (body_of_type ar) in let kelim = allowed_sorts issmall isunit ar_sort in let lc_bodies = Array.map body_of_type lc in - let splayed_lc = Array.map (splay_prod env Evd.empty) lc_bodies in - let nf_lc = Array.map (fun (d,b) -> prod_it b d) splayed_lc in + let splayed_lc = Array.map (splay_prod_assum env Evd.empty) lc_bodies in + let nf_lc = Array.map + (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in let nf_typed_lc,user_lc = if nf_lc = lc_bodies then lc,None else |