diff options
| author | mohring | 2000-12-06 08:50:51 +0000 |
|---|---|---|
| committer | mohring | 2000-12-06 08:50:51 +0000 |
| commit | 908672c4eb9bba99c43e8bb2a7376656429af6d7 (patch) | |
| tree | b09ee43dd297c7726cbf3be89a34cbcdc280ecd6 /kernel/indtypes.ml | |
| parent | 3fd9c34319dcfa7e05d70e26f55ea1350e13e72b (diff) | |
Reparation conditions de positivites inductifs, echange dans add_entry
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1057 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f05d4922d3..ece400ad16 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -184,17 +184,20 @@ let listrec_mconstr env ntypes nparams i indlc = if k >= n && k<n+ntypes then begin check_correct_par env nparams ntypes n (k-n+1) largs; Mrec(n+ntypes-k-1) - end else if noccur_between n ntypes x then + end else if List.for_all (noccur_between n ntypes) largs then if (n-nparams) <= k & k <= (n-1) then Param(n-1-k) else Norec else raise (IllFormedInd (LocalNonPos n)) | IsMutInd (ind_sp,a) -> - if (noccur_between n ntypes x) then Norec + if array_for_all (noccur_between n ntypes) a + && List.for_all (noccur_between n ntypes) largs + then Norec else Imbr(ind_sp,imbr_positive env n (ind_sp,a) largs) | err -> - if noccur_between n ntypes x then Norec + if noccur_between n ntypes x && List.for_all (noccur_between n ntypes) largs + then Norec else raise (IllFormedInd (LocalNonPos n)) and imbr_positive env n mi largs = @@ -210,6 +213,8 @@ let listrec_mconstr env ntypes nparams i indlc = (* The abstract imbricated inductive type with parameters substituted *) let auxlcvect = abstract_mind_lc env auxntyp auxnpar auxlc in let newidx = n + auxntyp in +(* Extends the environment with a variable corresponding to the inductive def *) + let env' = push_rel_assum (Anonymous,mis_user_arity mispeci) env in let _ = (* fails if the inductive type occurs non positively *) (* when substituted *) @@ -217,7 +222,7 @@ let listrec_mconstr env ntypes nparams i indlc = (function c -> let c' = hnf_prod_applist env Evd.empty c (List.map (lift auxntyp) lpar) in - check_construct env false newidx c') + check_construct env' false newidx c') auxlcvect in lrecargs |