diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-06 16:07:50 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-06 16:07:50 +0000 |
| commit | c7b600aa934cc245f7b8a58187833b6b45a2bee4 (patch) | |
| tree | 2108b365b10dae49575d4e520f134defd6af0e41 | |
| parent | 84c0f274e3baa424299c7b098ad7ced9ea4bab0e (diff) | |
check_correct_par n'etait pas fait au bon endroit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@213 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | kernel/indtypes.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 1dc9bdcd0..a34c98832 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -110,10 +110,10 @@ let listrec_mconstr env ntypes nparams i indlc = and largs = array_tl cl in (match hd with | Rel k -> - check_correct_par env nparams ntypes n (k-n+1) largs; - if k >= n && k<n+ntypes then + if k >= n && k<n+ntypes then begin + check_correct_par env nparams ntypes n (k-n+1) largs; Mrec(n+ntypes-k-1) - else if noccur_bet n ntypes x then + end else if noccur_bet n ntypes x then if (n-nparams) <= k & k <= (n-1) then Param(n-1-k) else Norec @@ -187,10 +187,10 @@ let listrec_mconstr env ntypes nparams i indlc = and largs = array_tl cl in (match hd with | Rel k -> - check_correct_par env nparams ntypes n (k-n+1) largs; - if k >= n & k<n+ntypes then + if k >= n & k<n+ntypes then begin + check_correct_par env nparams ntypes n (k-n+1) largs; Mrec(n+ntypes-k-1) - else if noccur_bet n ntypes x then + end else if noccur_bet n ntypes x then if (n-nparams) <= k & k <= (n-1) then Param(n-1-k) else Norec @@ -221,10 +221,11 @@ let listrec_mconstr env ntypes nparams i indlc = if check then (match hd with | Rel k -> - check_correct_par env nparams ntypes n (k-n+1) largs; - if k = n+ntypes-i then + if k = n+ntypes-i then begin + check_correct_par env nparams + ntypes n (k-n+1) largs; List.rev lrec - else + end else raise (IllFormedInd (NonPos n)) | _ -> raise (IllFormedInd (NonPos n))) else |