modules Indrec, Tacentries, Hiddentac

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@131 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 198 insertions, 224 deletions

diff --git a/library/declare.ml b/library/declare.ml
index ff006625a1..00f1fbf8d8 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -175,7 +175,7 @@ let global_reference kind id =
 let is_global id =
   try 
     let osp = Nametab.sp_of_id CCI id in
-    prefix_of (dirpath osp) (Lib.cwd())
+    list_prefix_of (dirpath osp) (Lib.cwd())
   with Not_found -> 
     false
 
diff --git a/library/global.ml b/library/global.ml
index 63efdbe4d9..e6c4008067 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open Util
 open Generic
 open Term
 open Instantiate
@@ -52,29 +53,9 @@ let mind_is_recursive = Util.compose mis_is_recursive lookup_mind_specif
 let mind_nconstr = Util.compose mis_nconstr lookup_mind_specif
 let mind_nparams = Util.compose mis_nparams lookup_mind_specif
 
-let mis_arity' mis =
-  let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
-  and largs = Array.to_list mis.mis_args in 
-  { body = instantiate_constr idhyps mis.mis_mip.mind_arity.body largs;
-    typ = mis.mis_mip.mind_arity.typ }
-
-let mis_arity mispec =
-  let { body = b; typ = t } = mis_arity' mispec in
-  DOP2 (Cast, b, DOP0 (Sort t))
-
 let mind_arity = Util.compose mis_arity lookup_mind_specif
 
-let mis_lc mis = 
-  instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps)
-    mis.mis_mip.mind_lc (Array.to_list mis.mis_args)
-
-let mis_lc_without_abstractions mis = 
-  let rec strip_DLAM = function
-    | (DLAM (n,c1)) -> strip_DLAM c1 
-    | (DLAMV (n,v)) -> v
-    | _ -> assert false
-  in 
-  strip_DLAM (mis_lc mis)
-
 let mind_lc_without_abstractions = 
   Util.compose mis_lc_without_abstractions lookup_mind_specif
+
+
diff --git a/library/global.mli b/library/global.mli
index 5a788f1f93..4e186d35b5 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -48,4 +48,3 @@ val mind_arity : constr -> constr
 
 val mind_lc_without_abstractions : constr -> constr array
 
-
diff --git a/library/indrec.ml b/library/indrec.ml
index 788e405f95..3aaa2214d9 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -7,11 +7,11 @@ open Names
 open Generic
 open Term
 open Inductive
+open Instantiate
 open Environ
 open Reduction
-open Typing
-
-let whd_betadeltaiota_empty env = whd_betadeltaiota env Evd.empty
+open Typeops
+open Type_errors
 
 let make_lambda_string s t c = DOP2(Lambda,t,DLAM(Name(id_of_string s),c))
 
@@ -21,60 +21,59 @@ let lift_context n l =
   let k = List.length l in 
   list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l
 
+let prod_create env (a,b) = 
+  mkProd (named_hd env a Anonymous) a b
+let lambda_name env (n,a,b) = 
+  mkLambda (named_hd env a n) a b
+let lambda_create env (a,b) = 
+  mkLambda (named_hd env a Anonymous) a b
+let it_prod_name env = 
+  List.fold_left (fun c (n,t) -> prod_name env (n,t,c)) 
+let it_lambda_name env = 
+  List.fold_left (fun c (n,t) -> lambda_name env (n,t,c))
+
 (*******************************************)
 (* Building curryfied elimination          *)
 (*******************************************)
 
-(*********************************************)
-(* lc is the list of the constructors of ind *)
-(*********************************************)
+(* (lc is the list of the constructors of ind) *)
 
-let mis_make_case_com depopt sigma mispec kinds =
+let mis_make_case_com depopt env sigma mispec kinds =
   let sp = mispec.mis_sp in
   let tyi = mispec.mis_tyi in 
   let cl = mispec.mis_args in 
   let nparams = mis_nparams mispec in
   let mip = mispec.mis_mip in
   let mind = DOPN(MutInd(sp,tyi),cl) in
-  let kd = mis_kd mispec in
-  let kn = mis_kn mispec in
+  let kelim = mis_kelim mispec in
   let t = mis_arity mispec in
   let (lc,lct) = mis_type_mconstructs mispec in
-  let lnames,sort = splay_prod sigma t in
+  let lnames,sort = splay_prod env sigma t in
   let nconstr = Array.length lc in
   let dep = match depopt with 
     | None -> (sort<>DOP0(Sort(Prop Null)))
     | Some d -> d
   in
-  let _ =
-    if dep then begin
-      if not (List.exists (sort_cmp CONV_X kinds) kd) then 
-       	let pm = pTERM mind in
-       	let ps = pTERM (DOP0(Sort kinds)) in
-       	errorlabstrm "Case analysis"
-          [< 'sTR "Dependent case analysis on sort: "; ps; 'fNL;
-             'sTR "is not allowed for inductive definition: "; pm >]
-    end else if not (List.exists (sort_cmp CONV_X kinds) kn) then 
-      let pm = pTERM mind in
-      let ps = pTERM (DOP0(Sort kinds)) in
-      errorlabstrm "Case analysis"
-       	[< 'sTR "Non Dependent case analysis on sort: "; ps; 'fNL;
-           'sTR "is not allowed for inductive definition: "; pm >]
-  in
-  let lnamesar,lnamespar = chop_list (List.length lnames - nparams) lnames in
+  if not (List.exists (base_sort_cmp CONV kinds) kelim) then begin
+    errorlabstrm "Case analysis"
+      [< 'sTR (if dep then "Dependent" else "Non Dependent");
+	 'sTR " case analysis on sort: "; print_sort kinds; 'fNL;
+         'sTR "is not allowed for inductive definition: "; print_sp sp >]
+  end;
+  let lnamesar,lnamespar = list_chop (List.length lnames - nparams) lnames in
   let lgar = List.length lnamesar in
-  let ar = hnf_prod_appvect sigma "make_case_dep" t (rel_vect 0 nparams) in
+  let ar = hnf_prod_appvect env sigma "make_case_dep" t (rel_vect 0 nparams) in
   let typP = 
     if dep then 
-      make_arity_dep (DOP0(Sort kinds)) ar 
+      make_arity_dep env sigma (DOP0(Sort kinds)) ar 
        	(appvect (mind,rel_vect 0 nparams))
     else 
-      make_arity_nodep (DOP0(Sort kinds)) ar 
+      make_arity_nodep env sigma (DOP0(Sort kinds)) ar 
   in 
   let rec add_branch k = 
     if k = nconstr then 
-      it_lambda_name 
-       	(lambda_create 
+      it_lambda_name env
+       	(lambda_create env
            (appvect (mind,
                      (Array.append (rel_vect (nconstr+lgar+1) nparams)
                        	(rel_vect 0 lgar))),
@@ -89,20 +88,19 @@ let mis_make_case_com depopt sigma mispec kinds =
     else 
       make_lambda_string "f" 
        	(if dep then 
-	   type_one_branch_dep 
-             (sigma,nparams,(rel_list (k+1) nparams),Rel (k+1)) lc.(k) lct.(k)
+	   type_one_branch_dep env sigma
+             (nparams,(rel_list (k+1) nparams),Rel (k+1)) lc.(k) lct.(k)
          else 
-	  type_one_branch_nodep 
-            (sigma,nparams,(rel_list (k+1) nparams),Rel (k+1)) lct.(k))
+	  type_one_branch_nodep env sigma
+            (nparams,(rel_list (k+1) nparams),Rel (k+1)) lct.(k))
        	(add_branch (k+1))
   in 
-  it_lambda_name (make_lambda_string "P" typP (add_branch 0)) lnamespar
+  it_lambda_name env (make_lambda_string "P" typP (add_branch 0)) lnamespar
     
-let make_case_com depopt sigma mind kinds =
-  let ity = mrectype_spec sigma mind in
-  let (sp,tyi,cl) = destMutInd ity in
-  let mispec = mind_specif_of_mind ity in 
-  mis_make_case_com depopt sigma mispec kinds
+let make_case_com depopt env sigma mind kinds =
+  let ity = mrectype_spec env sigma mind in
+  let mispec = lookup_mind_specif ity env in 
+  mis_make_case_com depopt env sigma mispec kinds
 
 let make_case_dep sigma   = make_case_com (Some true) sigma
 let make_case_nodep sigma = make_case_com (Some false) sigma 
@@ -126,18 +124,18 @@ let make_case_gen sigma   = make_case_com None sigma
 ************************************************************************)
 
 let simple_prod (n,t,c) = DOP2(Prod,t,DLAM(n,c))
-let make_prod_dep dep = if dep then prod_name else simple_prod
+let make_prod_dep dep env = if dep then prod_name env else simple_prod
 
-let type_rec_branch dep (sigma,vargs,depPvect,decP) co t recargs = 
+let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs = 
   let make_prod = make_prod_dep dep in
   let nparams = Array.length vargs in
-  let st = hnf_prod_appvect sigma "type_rec_branch" t vargs in
+  let st = hnf_prod_appvect env sigma "type_rec_branch" t vargs in
   let process_pos depK pk = 
     let rec prec i p = 
-      match whd_betadeltaiota_stack sigma p [] with 
-	| (DOP2(Prod,t,DLAM(n,c))),[] -> make_prod (n,t,prec (i+1) c)
+      match whd_betadeltaiota_stack env sigma p [] with 
+	| (DOP2(Prod,t,DLAM(n,c))),[] -> make_prod env (n,t,prec (i+1) c)
      	| (DOPN(MutInd _,_),largs) -> 
-	    let (_,realargs) = chop_list nparams largs in 
+	    let (_,realargs) = list_chop nparams largs in 
 	    let base = applist (lift i pk,realargs) in       
             if depK then 
 	      mkAppList base [appvect (Rel (i+1),rel_vect 0 i)]
@@ -148,7 +146,7 @@ let type_rec_branch dep (sigma,vargs,depPvect,decP) co t recargs =
     prec 0 
   in
   let rec process_constr i c recargs co = 
-    match whd_betadeltaiota_stack sigma c [] with 
+    match whd_betadeltaiota_stack env sigma c [] with 
       | (DOP2(Prod,t,DLAM(n,c_0)),[]) -> 
           let (optionpos,rest) = 
 	    match recargs with 
@@ -161,34 +159,34 @@ let type_rec_branch dep (sigma,vargs,depPvect,decP) co t recargs =
 	  in 
           (match optionpos with 
 	     | None -> 
-		 make_prod (n,t,process_constr (i+1) c_0 rest 
-                              (mkAppList (lift 1 co) [Rel 1]))
+		 make_prod env (n,t,process_constr (i+1) c_0 rest 
+				  (mkAppList (lift 1 co) [Rel 1]))
              | Some(dep',p) -> 
 		 let nP = lift (i+1+decP) p in
 		 let t_0 = process_pos dep' nP (lift 1 t) in 
-		 make_prod_dep (dep or dep')
+		 make_prod_dep (dep or dep') env
                    (n,t,mkArrow t_0 (process_constr (i+2) (lift 1 c_0) rest
 				       (mkAppList (lift 2 co) [Rel 2]))))
       | (DOPN(MutInd(_,tyi),_),largs) -> 
       	  let nP = match depPvect.(tyi) with 
 	    | Some(_,p) -> lift (i+decP) p
 	    | _ -> assert false in
-      	  let (_,realargs) = chop_list nparams largs in
+      	  let (_,realargs) = list_chop nparams largs in
       	  let base = applist (nP,realargs) in
           if dep then mkAppList base [co] else base
       | _ -> assert false
   in 
   process_constr 0 st recargs (appvect(co,vargs))
 
-let rec_branch_arg (sigma,vargs,fvect,decF) f t recargs = 
+let rec_branch_arg env sigma (vargs,fvect,decF) f t recargs = 
   let nparams = Array.length vargs in
-  let st = hnf_prod_appvect sigma "type_rec_branch" t vargs in
+  let st = hnf_prod_appvect env sigma "type_rec_branch" t vargs in
   let process_pos fk  = 
     let rec prec i p = 
-      (match whd_betadeltaiota_stack sigma p [] with 
-	 | (DOP2(Prod,t,DLAM(n,c))),[] -> lambda_name (n,t,prec (i+1) c) 
+      (match whd_betadeltaiota_stack env sigma p [] with 
+	 | (DOP2(Prod,t,DLAM(n,c))),[] -> lambda_name env (n,t,prec (i+1) c) 
      	 | (DOPN(MutInd _,_),largs) -> 
-             let (_,realargs) = chop_list nparams largs
+             let (_,realargs) = list_chop nparams largs
              and arg = appvect (Rel (i+1),rel_vect 0 i) in 
              applist(lift i fk,realargs@[arg])
      	 | _ -> assert false) 
@@ -196,7 +194,7 @@ let rec_branch_arg (sigma,vargs,fvect,decF) f t recargs =
     prec 0 
   in
   let rec process_constr i c f recargs = 
-    match whd_betadeltaiota_stack sigma c [] with 
+    match whd_betadeltaiota_stack env sigma c [] with 
       | (DOP2(Prod,t,DLAM(n,c_0)),[]) -> 
           let (optionpos,rest) = 
 	    match recargs with 
@@ -208,29 +206,31 @@ let rec_branch_arg (sigma,vargs,fvect,decF) f t recargs =
 	  in 
           (match optionpos with 
              | None -> 
-		 lambda_name 
+		 lambda_name env
 		   (n,t,process_constr (i+1) c_0 
-		      (applist(whd_beta_stack (lift 1 f) [(Rel 1)])) rest)
+		      (applist(whd_beta_stack env sigma (lift 1 f) 
+				 [(Rel 1)])) rest)
              | Some(_,f_0) -> 
 		 let nF = lift (i+1+decF) f_0 in
 		 let arg = process_pos nF (lift 1 t) in 
-                 lambda_name 
+                 lambda_name env
 		   (n,t,process_constr (i+1) c_0 
-		      (applist(whd_beta_stack (lift 1 f) [(Rel 1); arg])) 
+		      (applist(whd_beta_stack env sigma (lift 1 f) 
+				 [(Rel 1); arg])) 
 		      rest))
       | (DOPN(MutInd(_,tyi),_),largs) -> f
       | _ -> assert false
   in 
   process_constr 0 st f recargs 
 
-let mis_make_indrec sigma listdepkind mispec =
+let mis_make_indrec env sigma listdepkind mispec =
   let nparams = mis_nparams mispec in
   let recargsvec = mis_recargs mispec in
   let ntypes = mis_ntypes mispec in
   let mind_arity = mis_arity mispec in 
-  let (lnames, ckind) = splay_prod sigma mind_arity in
+  let (lnames, ckind) = splay_prod env sigma mind_arity in
   let kind = destSort ckind in
-  let lnamespar = lastn nparams lnames in
+  let lnamespar = list_lastn nparams lnames in
   let listdepkind = 
     if listdepkind = [] then 
       let dep = kind <> Prop Null in [(mispec,dep,kind)] 
@@ -244,7 +244,7 @@ let mis_make_indrec sigma listdepkind mispec =
       assign k = function 
 	| [] -> ()
         | (mispeci,dep,_)::rest -> 
-            (Array.set depPvec mispeci.tyi (Some(dep,Rel k));
+            (Array.set depPvec mispeci.mis_tyi (Some(dep,Rel k));
              assign (k-1) rest)
     in 
     assign nrec listdepkind  
@@ -253,30 +253,30 @@ let mis_make_indrec sigma listdepkind mispec =
     let makefix nbconstruct = 
       let rec mrec i ln ltyp ldef = function 
 	| (mispeci,dep,_)::rest -> 
-	    let tyi = mispeci.tyi in
-	    let mind = DOPN(MutInd (mispeci.sp,tyi),mispeci.args) in
+	    let tyi = mispeci.mis_tyi in
+	    let mind = DOPN(MutInd (mispeci.mis_sp,tyi),mispeci.mis_args) in
 	    let (_,lct) = mis_type_mconstructs mispeci in
 	    let nctyi = Array.length lct in (* nb constructeurs du type *) 
-	    let realar =  hnf_prod_appvect sigma "make_branch" 
+	    let realar =  hnf_prod_appvect env sigma "make_branch" 
 			    (mis_arity mispeci) 
 			    (rel_vect (nrec+nbconstruct) nparams) in
                (* arity in the contexte P1..Prec f1..f_nbconstruct *)
-	    let lnames,_ = splay_prod sigma realar in 
+	    let lnames,_ = splay_prod env sigma realar in 
 	    let nar = List.length lnames in 
 	    let decf = nar+nrec+nbconstruct+nrec in 
 	    let dect = nar+nrec+nbconstruct in
 	    let vecfi = rel_vect (dect+1-i-nctyi) nctyi in
 	    let branches = 
-	      map3_vect 
-		(rec_branch_arg (sigma,rel_vect (decf+1) nparams,
-				 depPvec,nar+1))
+	      array_map3
+		(rec_branch_arg env sigma 
+		   (rel_vect (decf+1) nparams,depPvec,nar+1))
                 vecfi lct recargsvec.(tyi) in
 	    let j = (match depPvec.(tyi) with 
 		       | Some (_,Rel j) -> j 
 		       | _ -> assert false) in
 	    let deftyi = 
-	      it_lambda_name 
-		(lambda_create 
+	      it_lambda_name env
+		(lambda_create env
 		   (appvect (mind,(Array.append (rel_vect decf nparams)
 				     (rel_vect 0 nar))),
 		    mkMutCaseA (ci_of_mind mind)
@@ -284,8 +284,8 @@ let mis_make_indrec sigma listdepkind mispec =
 		(lift_context nrec lnames)
 	    in
 	    let typtyi = 
-	      it_prod_name 
-		(prod_create 
+	      it_prod_name env
+		(prod_create env
 		   (appvect (mind,(Array.append (rel_vect dect nparams)
 				     (rel_vect 0 nar))),
 		    (if dep then 
@@ -301,7 +301,7 @@ let mis_make_indrec sigma listdepkind mispec =
             let fixdef = Array.of_list (List.rev ldef) in 
             let makefixdef = 
               put_DLAMSV 
-		(tabulate_list (fun _ -> Name(id_of_string "F")) nrec) fixdef 
+		(list_tabulate (fun _ -> Name(id_of_string "F")) nrec) fixdef 
 	    in 
             let fixspec = Array.append fixtyi [|makefixdef|] in 
 	    DOPN(Fix(fixn,p),fixspec)
@@ -310,7 +310,7 @@ let mis_make_indrec sigma listdepkind mispec =
     in 
     let rec make_branch i = function 
       | (mispeci,dep,_)::rest -> 
-	  let tyi = mispeci.tyi in
+	  let tyi = mispeci.mis_tyi in
 	  let (lc,lct) = mis_type_mconstructs mispeci in 
 	  let rec onerec j = 
 	    if j = Array.length lc then 
@@ -321,7 +321,7 @@ let mis_make_indrec sigma listdepkind mispec =
 	      let recarg = recargsvec.(tyi).(j) in
 	      let vargs = rel_vect (nrec+i+j) nparams in
 	      let p_0 = 
-		type_rec_branch dep (sigma,vargs,depPvec,i+j) co t recarg
+		type_rec_branch dep env sigma (vargs,depPvec,i+j) co t recarg
 	      in 
 	      DOP2(Lambda,p_0,DLAM(Name (id_of_string "f"),onerec (j+1)))
 	  in onerec 0
@@ -329,37 +329,37 @@ let mis_make_indrec sigma listdepkind mispec =
 	  makefix i listdepkind
     in 
     let rec put_arity i = function 
-      | ((mispeci,dep,kinds)::rest) -> 
-	  let mind = DOPN(MutInd (mispeci.sp,mispeci.tyi),mispeci.args) in 
+      | (mispeci,dep,kinds)::rest -> 
+	  let mind = DOPN(MutInd (mispeci.mis_sp,mispeci.mis_tyi),
+			  mispeci.mis_args) in 
 	  let arity = mis_arity mispeci in 
 	  let ar =
-	    hnf_prod_appvect sigma "put_arity" arity (rel_vect i nparams)
+	    hnf_prod_appvect env sigma "put_arity" arity (rel_vect i nparams)
 	  in 
 	  let typP = 
 	    if dep then 
-	      make_arity_dep (DOP0(Sort kinds)) ar 
+	      make_arity_dep env sigma (DOP0(Sort kinds)) ar 
 		(appvect (mind,rel_vect i nparams))
             else 
-	      make_arity_nodep (DOP0(Sort kinds)) ar 
+	      make_arity_nodep env sigma (DOP0(Sort kinds)) ar 
 	  in 
 	  DOP2(Lambda,typP,DLAM(Name(id_of_string "P"),put_arity (i+1) rest))
       | [] -> 
 	  make_branch 0 listdepkind 
     in 
     let (mispeci,dep,kind) = List.nth listdepkind p in
-    if is_recursive (List.map (fun (mispec,_,_) -> mispec.tyi) listdepkind)
-      recargsvec.(mispeci.tyi) then 
-   	it_lambda_name (put_arity 0 listdepkind) lnamespar
+    if is_recursive (List.map (fun (mispec,_,_) -> mispec.mis_tyi) listdepkind)
+      recargsvec.(mispeci.mis_tyi) then 
+   	it_lambda_name env (put_arity 0 listdepkind) lnamespar
    else 
-     mis_make_case_com (Some dep) sigma mispeci kind 
+     mis_make_case_com (Some dep) env sigma mispeci kind 
   in 
-  tabulate_vect make_one_rec nrec
+  Array.init nrec make_one_rec
 
-let make_indrec sigma listdepkind mind =
-  let ity = minductype_spec sigma mind in
-  let (sp,tyi,largs) = destMutInd ity in
-  let mispec = mind_specif_of_mind ity in  
-  mis_make_indrec sigma listdepkind mispec 
+let make_indrec env sigma listdepkind mind =
+  let ity = minductype_spec env sigma mind in
+  let mispec = lookup_mind_specif ity env in  
+  mis_make_indrec env sigma listdepkind mispec 
     
 let change_sort_arity sort = 
   let rec drec = function 
@@ -383,67 +383,55 @@ let instanciate_indrec_scheme sort =
 let check_arities listdepkind = 
   List.iter 
     (function (mispeci,dep,kinds) -> 
-       let mip = mispeci.mip  in
-       if dep then 
-	 let kd = mis_kd mispeci in 
-	 if List.exists (sort_cmp CONV_X kinds) kd then 
-	   ()
-	 else 
-	   errorlabstrm "Bad Induction"
-	     [<'sTR "Dependent induction for type "; 
-	       print_id mip.mINDTYPENAME;
-	       'sTR " and sort "; pTERM (DOP0(Sort kinds)); 
-	       'sTR "is not allowed">]
-       else 
-	 let kn = mis_kn mispeci in 
-	 if List.exists (sort_cmp CONV_X kinds) kn then 
-	   ()
-         else 
-	   errorlabstrm "Bad Induction"
-	     [<'sTR "Non dependent induction for type "; 
-	       print_id mip.mINDTYPENAME;
-	       'sTR " and sort "; pTERM (DOP0(Sort kinds)); 
-	       'sTR "is not allowed">])
+       let mip = mispeci.mis_mip  in
+       let kelim = mis_kelim mispeci in
+       if not (List.exists (base_sort_cmp CONV kinds) kelim) then 
+	 errorlabstrm "Bad Induction"
+	   [<'sTR (if dep then "Dependent" else "Non dependend");
+	     'sTR " induction for type "; 
+	     print_id mip.mind_typename;
+	     'sTR " and sort "; print_sort kinds; 
+	     'sTR "is not allowed">])
     listdepkind
 
-let build_indrec sigma = function 
-  | ((mind,dep,s)::lrecspec) ->
-      let redind = minductype_spec sigma mind in 
+let build_indrec env sigma = function 
+  | (mind,dep,s)::lrecspec ->
+      let redind = minductype_spec env sigma mind in 
       let (sp,tyi,_) = destMutInd redind in 
       let listdepkind = 
-    	(mind_specif_of_mind redind, dep,s)::
+    	(lookup_mind_specif redind env, dep,s)::
     	(List.map (function (mind',dep',s') ->
-		     let redind' = minductype_spec sigma mind' in
+		     let redind' = minductype_spec env sigma mind' in
 		     let (sp',_,_) = destMutInd redind' in
 		     if sp=sp' then 
-		       (mind_specif_of_mind redind',dep',s') 
+		       (lookup_mind_specif redind' env,dep',s') 
 		     else 
 		       error 
 			 "Induction schemes concern mutually inductive types") 
 	   lrecspec) 
       in
       let _ = check_arities listdepkind in 
-      make_indrec sigma listdepkind mind
+      make_indrec env sigma listdepkind mind
   | _ -> assert false
 	
 
 (* In order to interpret the Match operator *)
 
 let type_mutind_rec env sigma ct pt p c = 
-  let (mI,largs as mind) = find_minductype sigma ct in
-  let mispec = mind_specif_of_mind mI in 
-  let recargs =  mis_recarg mispec in
-  if is_recursive [mispec.tyi] recargs then
-    let dep = find_case_dep_mis env sigma mispec (c,p) mind pt in 
+  let (mI,largs as mind) = find_minductype env sigma ct in
+  let mispec = lookup_mind_specif mI env in 
+  let recargs = mis_recarg mispec in
+  if is_recursive [mispec.mis_tyi] recargs then
+    let (dep,_) = find_case_dep_nparams env sigma (c,p) mind pt in 
     let ntypes = mis_nconstr mispec 
-    and tyi = mispec.tyi 
+    and tyi = mispec.mis_tyi 
     and nparams = mis_nparams mispec in
     let depPvec = Array.create ntypes (None : (bool * constr) option) in 
-    let _ = Array.set depPvec mispec.tyi (Some(dep,p)) in 
-    let (pargs,realargs) = chop_list nparams largs in
+    let _ = Array.set depPvec mispec.mis_tyi (Some(dep,p)) in 
+    let (pargs,realargs) = list_chop nparams largs in
     let vargs = Array.of_list pargs in
     let (constrvec,typeconstrvec) = mis_type_mconstructs mispec in
-    let lft = map3_vect (type_rec_branch dep (sigma,vargs,depPvec,0)) 
+    let lft = array_map3 (type_rec_branch dep env sigma (vargs,depPvec,0)) 
                 constrvec typeconstrvec recargs in
     (mI, lft,
      if dep then applist(p,realargs@[c]) 
@@ -451,11 +439,11 @@ let type_mutind_rec env sigma ct pt p c =
   else 
     type_case_branches env sigma ct pt p c
 
-let is_mutind sigma ct =  
-  try let _ = find_minductype sigma ct in true with Induc -> false
+let is_mutind env sigma ct =  
+  try let _ = find_minductype env sigma ct in true with Induc -> false
 
-let type_rec_branches recursive sigma env ct pt p c = 
-  match whd_betadeltaiota_stack sigma ct [] with 
+let type_rec_branches recursive env sigma ct pt p c = 
+  match whd_betadeltaiota_stack env sigma ct [] with 
     | (DOPN(MutInd _,_),_) -> 
 	if recursive then 
 	  type_mutind_rec env sigma ct pt p c
@@ -468,7 +456,7 @@ let type_rec_branches recursive sigma env ct pt p c =
 
 let stacklamxtra recfun = 
   let rec lamrec sigma p_0 p_1 = match p_0,p_1 with 
-    | (stack, (DOP2(Lambda,DOP1(XTRA("COMMENT",[]),_),DLAM(_,c)) as t)) ->
+    | (stack, (DOP2(Lambda,DOP1(XTRA "COMMENT",_),DLAM(_,c)) as t)) ->
         recfun stack (substl sigma t)
     | ((h::t), (DOP2(Lambda,_,DLAM(_,c)))) -> lamrec (h::sigma) t c
     | (stack, t) -> recfun stack (substl sigma t)
@@ -477,55 +465,55 @@ let stacklamxtra recfun =
 
 let rec whrec x stack =
   match x with   
-    | DOP2(Lambda,DOP1(XTRA("COMMENT",[]),c),DLAM(name,t)) ->
+    | DOP2(Lambda,DOP1(XTRA "COMMENT",c),DLAM(name,t)) ->
     	let t' = applist (whrec t (List.map (lift 1) stack)) in 
-	DOP2(Lambda,DOP1(XTRA("COMMENT",[]),c),DLAM(name,t')),[]
+	DOP2(Lambda,DOP1(XTRA "COMMENT",c),DLAM(name,t')),[]
     | DOP2(Lambda,c1,DLAM(name,c2)) ->
     	(match stack with
 	   | [] -> (DOP2(Lambda,c1,DLAM(name,whd_betaxtra c2)),[])
 	   | a1::rest -> stacklamxtra (fun l x -> whrec x l) [a1] rest c2)
-    | DOPN(AppL,cl)      -> whrec (hd_vect cl) (app_tl_vect cl stack)
-    | DOP2(Cast,c,_)       ->  whrec c stack
+    | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack)
+    | DOP2(Cast,c,_) ->  whrec c stack
     | x -> x,stack
 
 and whd_betaxtra x = applist(whrec x [])
 
 let transform_rec env sigma cl (ct,pt) = 
-  let (mI,largs as mind) = find_minductype sigma ct in
+  let (mI,largs as mind) = find_minductype env sigma ct in
   let p = cl.(0)
   and c = cl.(1)
   and lf = Array.sub cl 2 ((Array.length cl) - 2) in
-  let mispec = mind_specif_of_mind mI in 
-  let recargs =  mis_recarg mispec in
+  let mispec = lookup_mind_specif mI env in 
+  let recargs = mis_recarg mispec in
   let expn = Array.length recargs in
   if Array.length lf <> expn then error_number_branches CCI env c ct expn;
-  if is_recursive [mispec.tyi] recargs then
-    let dep = find_case_dep_mis env sigma mispec (c,p) mind pt in 
+  if is_recursive [mispec.mis_tyi] recargs then
+    let (dep,_) = find_case_dep_nparams env sigma (c,p) mind pt in 
     let ntypes = mis_nconstr mispec 
-    and tyi = mispec.tyi 
+    and tyi = mispec.mis_tyi 
     and nparams = mis_nparams mispec in
     let depFvec = Array.create ntypes (None : (bool * constr) option) in 
-    let _ = Array.set depFvec mispec.tyi (Some(dep,Rel 1)) in 
-    let (pargs,realargs) = chop_list nparams largs in
+    let _ = Array.set depFvec mispec.mis_tyi (Some(dep,Rel 1)) in 
+    let (pargs,realargs) = list_chop nparams largs in
     let vargs = Array.of_list pargs in
     let (_,typeconstrvec) = mis_type_mconstructs mispec in
     (* build now the fixpoint *)
     let realar =
-      hnf_prod_appvect sigma "make_branch" (mis_arity mispec) vargs in
-    let lnames,_ = splay_prod sigma realar in 
+      hnf_prod_appvect env sigma "make_branch" (mis_arity mispec) vargs in
+    let lnames,_ = splay_prod env sigma realar in 
     let nar = List.length lnames in
     let branches = 
-      map3_vect 
+      array_map3
 	(fun f t reca -> 
 	   whd_betaxtra
-             (rec_branch_arg
-                (sigma,(Array.map (lift (nar+2)) vargs),depFvec,nar+1)
+             (rec_branch_arg env sigma
+                ((Array.map (lift (nar+2)) vargs),depFvec,nar+1)
                 f t reca))
         (Array.map (lift (nar+2)) lf) typeconstrvec recargs 
     in 
     let deffix = 
-      it_lambda_name 
-	(lambda_create 
+      it_lambda_name env
+	(lambda_create env
 	   (appvect (mI,Array.append (Array.map (lift (nar+1)) vargs)
                        (rel_vect 0 nar)),
             mkMutCaseA (ci_of_mind mI) 
@@ -533,17 +521,20 @@ let transform_rec env sigma cl (ct,pt) =
         (lift_context 1 lnames) 
     in
     if noccurn 1 deffix then 
-      whd_beta (applist (pop deffix,realargs@[c]))
+      whd_beta env sigma (applist (pop deffix,realargs@[c]))
     else
       let typPfix = 
-	it_prod_name  
-	  (prod_create (appvect (mI,(Array.append 
-				       (Array.map (lift nar) vargs)
-				       (rel_vect 0 nar))),
-			(if dep then applist (whd_beta_stack (lift (nar+1) p)
-                                                (rel_list 0 (nar+1)))
-			 else applist (whd_beta_stack (lift (nar+1) p) 
-                                         (rel_list 1 nar)))))
+	it_prod_name env
+	  (prod_create env
+	     (appvect (mI,(Array.append 
+			     (Array.map (lift nar) vargs)
+			     (rel_vect 0 nar))),
+	      (if dep then 
+		 applist (whd_beta_stack env sigma 
+			    (lift (nar+1) p) (rel_list 0 (nar+1)))
+	       else 
+		 applist (whd_beta_stack env sigma 
+			    (lift (nar+1) p) (rel_list 1 nar)))))
           lnames 
       in
       let fix = DOPN(Fix([|nar|],0),
@@ -556,9 +547,9 @@ let transform_rec env sigma cl (ct,pt) =
 
 (*** Building ML like case expressions without types ***)
 
-let concl_n sigma = 
+let concl_n env sigma = 
   let rec decrec m c = if m = 0 then c else 
-    match whd_betadeltaiota sigma c with
+    match whd_betadeltaiota env sigma c with
       | DOP2(Prod,_,DLAM(n,c_0)) -> decrec (m-1) c_0
       | _                        -> failwith "Typing.concl_n"
   in 
@@ -572,16 +563,16 @@ let count_rec_arg j =
   in 
   crec 0
     
-let norec_branch_scheme sigma typc =
-  let rec crec typc = match whd_betadeltaiota sigma typc with 
+let norec_branch_scheme env sigma typc =
+  let rec crec typc = match whd_betadeltaiota env sigma typc with 
     | DOP2(Prod,c,DLAM(name,t)) -> DOP2(Prod,c,DLAM(name,crec t))
     | _ -> mkExistential
   in 
   crec typc
 
-let rec_branch_scheme sigma j typc recargs = 
+let rec_branch_scheme env sigma j typc recargs = 
   let rec crec (typc,recargs) = 
-    match whd_betadeltaiota sigma typc, recargs with 
+    match whd_betadeltaiota env sigma typc, recargs with 
       | (DOP2(Prod,c,DLAM(name,t)),(ra::reca)) -> 
           DOP2(Prod,c,
 	       match ra with 
@@ -596,26 +587,27 @@ let rec_branch_scheme sigma j typc recargs =
   in 
   crec (typc,recargs) 
     
-let branch_scheme sigma isrec i mind = 
-  let typc =  type_inst_construct sigma i mind in 
+let branch_scheme env sigma isrec i mind = 
+  let typc = type_inst_construct env sigma i mind in 
   if isrec then
-    let (mI,_) = find_mrectype sigma mind in
+    let (mI,_) = find_mrectype env sigma mind in
     let (_,j,_) = destMutInd mI in
-    let mispec = mind_specif_of_mind mI in 
+    let mispec = lookup_mind_specif mI env in 
     let recarg = (mis_recarg mispec).(i-1) in
-    rec_branch_scheme sigma j typc recarg
+    rec_branch_scheme env sigma j typc recarg
   else 
-    norec_branch_scheme sigma typc
+    norec_branch_scheme env sigma typc
 
 (* if arity of mispec is (p_bar:P_bar)(a_bar:A_bar)s where p_bar are the
  * K parameters. Then then build_notdep builds the predicate
  * [a_bar:A'_bar](lift k pred) 
  * where A'_bar = A_bar[p_bar <- globargs] *)
 
-let build_notdep_pred mispec nparams globargs pred =
+let build_notdep_pred env sigma mispec nparams globargs pred =
   let arity = mis_arity mispec in
   let lamarity = to_lambda nparams arity in
-  let inst_arity = whd_beta (appvect (lamarity,Array.of_list globargs)) in
+  let inst_arity = 
+    whd_beta env sigma (appvect (lamarity,Array.of_list globargs)) in
   let k = nb_prod inst_arity in
   let env,_,npredlist = push_and_liftl k [] inst_arity [insert_lifted pred] in
   let npred = (match npredlist with [npred] -> npred 
@@ -624,20 +616,20 @@ let build_notdep_pred mispec nparams globargs pred =
   in 
   finalpred
 
-let pred_case_ml_fail sigma isrec ct (i,ft) =
+let pred_case_ml_fail env sigma isrec ct (i,ft) =
   try 
-    let (mI,largs) = find_mrectype sigma ct in
+    let (mI,largs) = find_mrectype env sigma ct in
     let (_,j,_) = destMutInd mI in
-    let mispec = mind_specif_of_mind mI in
+    let mispec = lookup_mind_specif mI env in
     let nparams = mis_nparams mispec in
-    let (globargs,la) = chop_list nparams largs in
+    let (globargs,la) = list_chop nparams largs in
     let pred = 
       let recargs = (mis_recarg mispec) in
       assert (Array.length recargs <> 0);
       let recargi = recargs.(i-1) in
       let nbrec = if isrec then count_rec_arg j recargi else 0 in
       let nb_arg = List.length (recargs.(i-1)) + nbrec in
-      let pred = concl_n sigma nb_arg ft in
+      let pred = concl_n env sigma nb_arg ft in
       if noccur_bet 1 nb_arg pred then 
 	lift (-nb_arg) pred
       else 
@@ -646,25 +638,25 @@ let pred_case_ml_fail sigma isrec ct (i,ft) =
     if la = [] then 
       pred
     else (* we try with [_:T1]..[_:Tn](lift n pred) *)
-      build_notdep_pred mispec nparams globargs pred  
+      build_notdep_pred env sigma mispec nparams globargs pred  
   with Induc -> 
     failwith "Inductive"
 
 let pred_case_ml env sigma isrec (c,ct) lf (i,ft) = 
   try 
-    pred_case_ml_fail sigma isrec ct (i,ft)
+    pred_case_ml_fail env sigma isrec ct (i,ft)
   with Failure mes -> 
-    error_ml_case mes env c ct lf.(i-1) ft
+    error_ml_case CCI env mes c ct lf.(i-1) ft
 
 (* similar to pred_case_ml but does not expect the list lf of braches *)
 let pred_case_ml_onebranch env sigma isrec (c,ct) (i,f,ft) = 
   try 
-    pred_case_ml_fail sigma isrec ct (i,ft)
+    pred_case_ml_fail env sigma isrec ct (i,ft)
   with Failure mes -> 
-    error_ml_case mes env c ct f ft
+    error_ml_case CCI env mes c ct f ft
       
 let make_case_ml isrec pred c ci lf = 
   if isrec then 
-    DOPN(XTRA("REC",[]),Array.append [|pred;c|] lf)
+    DOPN(XTRA("REC"),Array.append [|pred;c|] lf)
   else 
     mkMutCaseA ci pred c lf
diff --git a/library/indrec.mli b/library/indrec.mli
index 408c97e39f..04cd875729 100644
--- a/library/indrec.mli
+++ b/library/indrec.mli
@@ -11,19 +11,20 @@ open Evd
 
 (* Eliminations. *)
 
-val make_case_dep : 'c evar_map -> constr -> sorts -> constr
-val make_case_nodep : 'c evar_map -> constr -> sorts -> constr
-val make_case_gen : 'c evar_map -> constr -> sorts -> constr
+val make_case_dep : unsafe_env -> 'a evar_map -> constr -> sorts -> constr
+val make_case_nodep : unsafe_env -> 'a evar_map -> constr -> sorts -> constr
+val make_case_gen : unsafe_env -> 'a evar_map -> constr -> sorts -> constr
 
-val make_indrec : 'c evar_map -> (mind_specif * bool * sorts) list 
-  -> constr -> constr array
+val make_indrec : unsafe_env -> 'a evar_map -> 
+  (mind_specif * bool * sorts) list -> constr -> constr array
 
-val mis_make_indrec : 'c evar_map -> (mind_specif * bool * sorts) list 
-  -> mind_specif -> constr array
+val mis_make_indrec : unsafe_env -> 'a evar_map -> 
+  (mind_specif * bool * sorts) list -> mind_specif -> constr array
 
 val instanciate_indrec_scheme : sorts -> int -> constr -> constr
 
-val build_indrec : 'c evar_map -> (constr * bool * sorts) list -> constr array
+val build_indrec : 
+  unsafe_env -> 'a evar_map -> (constr * bool * sorts) list -> constr array
 
 val type_rec_branches : bool -> unsafe_env -> 'c evar_map -> constr 
   -> constr -> constr -> constr -> constr * constr array * constr
@@ -31,9 +32,10 @@ val type_rec_branches : bool -> unsafe_env -> 'c evar_map -> constr
 val transform_rec : unsafe_env -> 'c evar_map -> (constr array) 
   -> (constr * constr) -> constr
 
-val is_mutind : 'c evar_map -> constr -> bool 
+val is_mutind : unsafe_env -> 'a evar_map -> constr -> bool 
 
-val branch_scheme : 'c evar_map -> bool -> int -> constr -> constr
+val branch_scheme : 
+  unsafe_env -> 'a evar_map -> bool -> int -> constr -> constr
 
 val pred_case_ml : unsafe_env -> 'c evar_map -> bool -> (constr * constr) 
   ->  constr array -> (int*constr)  ->constr