From c7b600aa934cc245f7b8a58187833b6b45a2bee4 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 6 Dec 1999 16:07:50 +0000
Subject: 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
---
 kernel/indtypes.ml | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 1dc9bdcd06..a34c98832f 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 
-- 
cgit v1.2.3