From d44846131cf2fab2d3c45d435b84d802b1af8d43 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 15 Dec 1999 15:24:13 +0000
Subject: Nouveaux types 'constructor' et 'inductive' dans Term; les fonctions
 sur les inductifs prennent maintenant des 'inductive' en paramètres; elle
 n'ont plus besoin de faire des appels dangereux aux find_m*type qui
 centralisent la levée de raise Induc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/indtypes.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index da9604699c..cdb45e9d4a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -111,7 +111,7 @@ let listrec_mconstr env ntypes nparams i indlc =
                  let hd = array_hd cl 
 		 and largs = array_tl cl in
                  (match hd with 
-                    | Rel k -> 
+                    | Rel k ->
                         if k >= n && k<n+ntypes then begin
 			  check_correct_par env nparams ntypes n (k-n+1) largs;
 			  Mrec(n+ntypes-k-1) 
@@ -121,17 +121,17 @@ let listrec_mconstr env ntypes nparams i indlc =
                           else Norec
 			else 
 			  raise (IllFormedInd (NonPos n))
-                    | (DOPN(MutInd(sp,i),_) as mi) -> 
+                    | DOPN(MutInd ind_sp,a) -> 
                         if (noccur_bet n ntypes x) then
                           Norec
                         else 
-			  Imbr(sp,i,imbr_positive n mi largs)
+			  Imbr(ind_sp,imbr_positive n (ind_sp,a) largs)
                     | err -> 
 			if noccur_bet n ntypes x then Norec
 			else raise (IllFormedInd (NonPos n)))
              | _ -> anomaly "check_pos")
 	  
-  and imbr_positive n mi largs = 
+  and imbr_positive n mi largs =
     let mispeci = lookup_mind_specif mi env in
     let auxnpar = mis_nparams mispeci in
     let (lpar,auxlargs) = array_chop auxnpar largs in 
@@ -197,10 +197,10 @@ let listrec_mconstr env ntypes nparams i indlc =
                           then Param(n-1-k)
                           else Norec
 			else raise (IllFormedInd (NonPos n))
-                    | (DOPN(MutInd(sp,i),_) as mi) -> 
+                    | DOPN(MutInd ind_sp,a) -> 
                         if (noccur_bet n ntypes x) 
                         then Norec
-                        else Imbr(sp,i,imbr_positive n mi largs)
+                        else Imbr(ind_sp,imbr_positive n (ind_sp,a) largs)
                     | err -> if noccur_bet n ntypes x then Norec
 		      else raise (IllFormedInd (NonPos n)))
              | _ -> anomaly "check_param_pos")
@@ -249,7 +249,7 @@ let listrec_mconstr env ntypes nparams i indlc =
 let is_recursive listind =
   let rec one_is_rec rvec = 
     List.exists (function Mrec(i) -> List.mem i listind 
-                   | Imbr(_,_,lvec) -> one_is_rec lvec
+                   | Imbr(_,lvec) -> one_is_rec lvec
                    | Norec -> false
                    | Param _ -> false) rvec
   in 
-- 
cgit v1.2.3