Minor code cleaning in CArray / CList.

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

8 files changed, 10 insertions, 11 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 20cf9edb8..a5baa00f9 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -365,7 +365,7 @@ let discriminate_tac cstr p gls =
 let build_term_to_complete uf meta pac =
   let cinfo = get_constructor_info uf pac.cnode in
   let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
-  let dummy_args = List.rev (List.tabulate meta pac.arity) in
+  let dummy_args = List.rev (List.init pac.arity meta) in
   let all_args = List.rev_append real_args dummy_args in
     applistc (mkConstruct cinfo.ci_constr) all_args
 
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 3cc0686ad..9d34dc99a 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -341,9 +341,8 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	(fun (loc,(id,_)) ->
 	   GVar (loc,id)) params in
     let dum_args=
-      List.tabulate
-	(fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false)))
-	oib.Declarations.mind_nrealargs in
+      List.init oib.Declarations.mind_nrealargs
+	(fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false))) in
       glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in
   let pat_vars,aliases,patt = interp_pattern env pat in
   let inject = function
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 1ae8419c8..2ef2c9756 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1190,7 +1190,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	  match List.assoc id args with
 	      [None,br_args] -> 
 		let all_metas = 
-		  List.tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps)  in
+		  List.init (nparams + nhyps) (fun n -> mkMeta (succ n))  in
 		let param_metas,hyp_metas = List.chop nparams all_metas in
 		  tclTHEN
 		    (tclDO nhrec introf)
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index baf1972e6..12b2304ac 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -112,7 +112,7 @@ let mk_open_instance id gl m t=
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
-  let revt=substl (List.tabulate (fun i->mkRel (m-i)) m) t in
+  let revt=substl (List.init m (fun i->mkRel (m-i))) t in
   let rec aux n avoid=
     if n=0 then [] else
       let nid=(fresh_id avoid var_id gl) in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index c812deaf5..8abf9d7e2 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -129,7 +129,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
        let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
 	 it_mkLambda_or_LetIn head rc in
        let lp=Array.length rcs in
-       let newhyps=List.tabulate myterm lp in
+       let newhyps=List.init lp myterm in
 	 tclIFTHENELSE
 	   (tclTHENLIST
 	      [generalize newhyps;
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 238813e39..4e4a6f19f 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -189,8 +189,8 @@ let empty_seq depth=
 let expand_constructor_hints =
   List.map_append (function
     | IndRef ind ->
-	List.tabulate (fun i -> ConstructRef (ind,i+1))
-	  (Inductiveops.nconstructors ind)
+        List.init (Inductiveops.nconstructors ind)
+          (fun i -> ConstructRef (ind,i+1))
     | gr ->
 	[gr])
 
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 93f84687e..75fd0261a 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -124,7 +124,7 @@ let unif_atoms i dom t1 t2=
     | Not_found ->Some (Phantom dom)
 
 let renum_metas_from k n t= (* requires n = max (free_rels t) *)
-  let l=List.tabulate (fun i->mkMeta (k+i)) n in
+  let l=List.init n (fun i->mkMeta (k+i)) in
     substl l t
 
 let more_general (m1,t1) (m2,t2)=
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index a0f565ce3..1b2ba0e87 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -179,7 +179,7 @@ let dummy_goal env =
    Evd.sigma = sigma}
 
 let exec_tactic env n f args =
-  let lid = List.tabulate(fun i -> Id.of_string("x"^string_of_int i)) n in
+  let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
   let res = ref [||] in
   let get_res ist =
     let l = List.map (fun id ->  List.assoc id ist.lfun) lid in