From 914d19f19cd73d1794c0160bd6e7358c13eba630 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sat, 23 Mar 2013 15:05:26 +0000
Subject: Minor code cleaning in CArray / CList.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/coercion.ml     | 2 +-
 pretyping/detyping.ml     | 4 ++--
 pretyping/indrec.ml       | 2 +-
 pretyping/inductiveops.ml | 2 +-
 pretyping/reductionops.ml | 4 ++--
 pretyping/tacred.ml       | 4 ++--
 6 files changed, 9 insertions(+), 9 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 9c61d3f060..7d2ad487c9 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -52,7 +52,7 @@ let apply_pattern_coercion loc pat p =
   List.fold_left
     (fun pat (co,n) ->
        let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in
-	 Glob_term.PatCstr (loc, co, List.tabulate f (n+1), Anonymous))
+	 Glob_term.PatCstr (loc, co, List.init (n+1) f, Anonymous))
     pat p
 
 (* raise Not_found if no coercion found *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 89e6bf8225..cc900adb45 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -240,8 +240,8 @@ let rec build_tree na isgoal e ci cl =
   let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in
   let cnl = ci.ci_cstr_ndecls in
   List.flatten
-    (List.tabulate (fun i -> contract_branch isgoal e (cnl.(i),mkpat i,cl.(i)))
-       (Array.length cl))
+    (List.init (Array.length cl)
+      (fun i -> contract_branch isgoal e (cnl.(i),mkpat i,cl.(i))))
 
 and align_tree nal isgoal (e,c as rhs) = match nal with
   | [] -> [[],rhs]
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index a5c4ecd3b7..8904e2b7b2 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -432,7 +432,7 @@ let mis_make_indrec env sigma listdepkind mib =
 	mis_make_case_com dep env sigma indi (mibi,mipi) kind
   in
     (* Body of mis_make_indrec *)
-    List.tabulate make_one_rec nrec
+    List.init nrec make_one_rec
 
 (**********************************************************************)
 (* This builds elimination predicate for Case tactic *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index ef95fbb5c8..610bde6877 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -92,7 +92,7 @@ let mis_nf_constructor_type (ind,mib,mip) j =
   and nconstr = Array.length mip.mind_consnames in
   let make_Ik k = mkInd ((fst ind),ntypes-k-1) in
   if j > nconstr then error "Not enough constructors in the type.";
-  substl (List.tabulate make_Ik ntypes) specif.(j-1)
+  substl (List.init ntypes make_Ik) specif.(j-1)
 
 (* Arity of constructors excluding parameters and local defs *)
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 732001fde6..24ae6c1d0c 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -293,7 +293,7 @@ let contract_cofix ?env (bodynum,(names,types,bodies as typedbodies)) cst =
       match env with
       | None -> bd
       | Some e -> magicaly_constant_of_fixbody e bd names.(ind) in
-  let closure = List.tabulate make_Fi nbodies in
+  let closure = List.init nbodies make_Fi in
   substl closure bodies.(bodynum)
 
 let reduce_mind_case mia =
@@ -322,7 +322,7 @@ let contract_fix ?env ((recindices,bodynum),(names,types,bodies as typedbodies))
 	match env with
 	| None -> bd
 	| Some e -> magicaly_constant_of_fixbody e bd names.(ind) in
-    let closure = List.tabulate make_Fi nbodies in
+    let closure = List.init nbodies make_Fi in
     substl closure bodies.(bodynum)
 
 let fix_recarg ((recindices,bodynum),_) stack =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 508569f0d7..b46b69c624 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -457,7 +457,7 @@ let contract_fix_use_function env sigma f
   ((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
   let nbodies = Array.length recindices in
   let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
-  let lbodies = List.tabulate make_Fi nbodies in
+  let lbodies = List.init nbodies make_Fi in
   substl_checking_arity env (List.rev lbodies) (nf_beta sigma bodies.(bodynum))
 
 let reduce_fix_use_function env sigma f whfun fix stack =
@@ -480,7 +480,7 @@ let contract_cofix_use_function env sigma f
   (bodynum,(_names,_,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
   let make_Fi j = (mkCoFix(j,typedbodies), f j) in
-  let subbodies = List.tabulate make_Fi nbodies in
+  let subbodies = List.init nbodies make_Fi in
   substl_checking_arity env (List.rev subbodies)
     (nf_beta sigma bodies.(bodynum))
 
-- 
cgit v1.2.3