diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-24 16:33:01 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-24 16:33:01 +0000 |
| commit | 0b6a729e05b0b120f8d0a34b135bb0cf7e5bab82 (patch) | |
| tree | 5f6a043336474277a3767e162b128b9897ebcd87 /kernel/indtypes.ml | |
| parent | 678868fa553790aed94e68f77f340f407a48b3fd (diff) | |
Cas LetIn superflu dans check_construct car normalisation préalable
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2428 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 6ea71e09a..07608a4b9 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -421,17 +421,6 @@ let listrec_mconstr env ntypes hyps nparams i indlc = check_constr_rec (push_rel (na, None, b) env) (recarg::lrec) (n+1) d - (* LetIn's must be free of occurrence of the inductive types and - they do not contribute to recargs *) - | LetIn (na,b,t,d) -> - assert (largs = []); - if not (noccur_between n ntypes b & noccur_between n ntypes t) then - check_constr_rec (push_rel (na,Some b, b) env) - lrec n (subst1 b d) - else - let recarg = check_pos env n b in - check_constr_rec (push_rel (na,Some b, b) env) - lrec (n+1) d | hd -> if check_head then if hd = Rel (n+ntypes-i) then |