As r15801: putting everything from Util.array_* to CArray.*.

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

17 files changed, 46 insertions, 54 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 8af15a1d5..04038b1a7 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -396,7 +396,7 @@ let rec canonize_name c =
       | LetIn (na,b,t,ct) ->
 	  mkLetIn (na, func b,func t,func ct)
       | App (ct,l) ->
-	  mkApp (func ct,array_smartmap func l)
+	  mkApp (func ct,Array.smartmap func l)
       | _ -> c
 
 (* rebuild a term from a pattern and a substitution *)
@@ -502,7 +502,7 @@ let is_redundant state id args =
     let prev_args = Identhash.find_all state.q_history id in
     List.exists
       (fun old_args ->
-	 Util.array_for_all2 (fun i j -> i = find state.uf j)
+	 Util.Array.for_all2 (fun i j -> i = find state.uf j)
          norm_args old_args)
       prev_args
     with Not_found -> false
@@ -518,7 +518,7 @@ let add_inst state (inst,int_subst) =
       let subst = build_subst (forest state) int_subst in
       let prfhead= mkVar inst.qe_hyp_id in
       let args = Array.map constr_of_term subst in
-      let _ = array_rev args in (* highest deBruijn index first *)
+      let _ = Array.rev args in (* highest deBruijn index first *)
       let prf= mkApp(prfhead,args) in
 	  let s = inst_pattern subst inst.qe_lhs
 	  and t = inst_pattern subst inst.qe_rhs in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 423c95509..3b2e42d4e 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -101,7 +101,7 @@ let rec pattern_of_constr env sigma c =
       App (f,args)->
 	let pf = decompose_term env sigma f in
 	let pargs,lrels = List.split
-	  (array_map_to_list (pattern_of_constr env sigma) args) in
+	  (Array.map_to_list (pattern_of_constr env sigma) args) in
 	  PApp (pf,List.rev pargs),
 	List.fold_left Intset.union Intset.empty lrels
     | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index b5cdec3ec..aaf6f2bd0 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -141,8 +141,8 @@ let check_fix env cb i =
 
 let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) =
   na1 = na2 &&
-  array_equal eq_constr ca1 ca2 &&
-  array_equal eq_constr ta1 ta2
+  Array.equal eq_constr ca1 ca2 &&
+  Array.equal eq_constr ta1 ta2
 
 let factor_fix env l cb msb =
   let _,recd as check = check_fix env cb 0 in
@@ -287,7 +287,7 @@ let rec extract_sfb env mp all = function
 	 let vl,recd,msb = factor_fix env l cb msb in
 	 let vc = Array.map (make_con mp empty_dirpath) vl in
 	 let ms = extract_sfb env mp all msb in
-	 let b = array_exists Visit.needed_con vc in
+	 let b = Array.exists Visit.needed_con vc in
 	 if all || b then
 	   let d = extract_fixpoint env vc recd in
 	   if (not b) && (logical_decl d) then ms
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index e1bbcf9c7..ef0de36f5 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -202,7 +202,7 @@ let oib_equal o1 o2 =
   o1.mind_consnames = o2.mind_consnames
 
 let mib_equal m1 m2 =
-  array_equal oib_equal m1.mind_packets m1.mind_packets &&
+  Array.equal oib_equal m1.mind_packets m1.mind_packets &&
   m1.mind_record = m2.mind_record &&
   m1.mind_finite = m2.mind_finite &&
   m1.mind_ntypes = m2.mind_ntypes &&
@@ -833,7 +833,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
   let metas = Array.map new_meta fi in
   metas.(i) <- mlt;
   let mle = Array.fold_left Mlenv.push_type mle metas in
-  let ei = array_map2 (extract_maybe_term env mle) metas ci in
+  let ei = Array.map2 (extract_maybe_term env mle) metas ci in
   MLfix (i, Array.map id_of_name fi, ei)
 
 (*S ML declarations. *)
@@ -859,7 +859,7 @@ let rec gentypvar_ok c = match kind_of_term c with
   | App (c,v) ->
       (* if all arguments are variables, these variables will
 	 disappear after extraction (see [empty_s] below) *)
-      array_for_all isRel v && gentypvar_ok c
+      Array.for_all isRel v && gentypvar_ok c
   | Cast (c,_,_) -> gentypvar_ok c
   | _ -> false
 
@@ -1053,9 +1053,9 @@ let logical_decl = function
   | Dterm (_,MLdummy,Tdummy _) -> true
   | Dtype (_,[],Tdummy _) -> true
   | Dfix (_,av,tv) ->
-      (array_for_all ((=) MLdummy) av) &&
-      (array_for_all isDummy tv)
-  | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
+      (Array.for_all ((=) MLdummy) av) &&
+      (Array.for_all isDummy tv)
+  | Dind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
 
 (*s Is a [ml_spec] logical ? *)
@@ -1063,5 +1063,5 @@ let logical_decl = function
 let logical_spec = function
   | Stype (_, [], Some (Tdummy _)) -> true
   | Sval (_,Tdummy _) -> true
-  | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
+  | Sind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 2bc2306f1..4fd9f17ee 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -224,7 +224,7 @@ and pp_fix par env i (ids,bl) args =
        (v 1 (str "let {" ++ fnl () ++
 	     prvect_with_sep (fun () -> str ";" ++ fnl ())
 	       (fun (fi,ti) -> pp_function env (pr_id fi) ti)
-	       (array_map2 (fun a b -> a,b) ids bl) ++
+	       (Array.map2 (fun a b -> a,b) ids bl) ++
 	     str "}") ++
         fnl () ++ str "in " ++ pp_apply (pr_id ids.(i)) false args))
 
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 3716695b8..01b98b131 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -524,7 +524,7 @@ let has_deep_pattern br =
     | Pcons (_,l) | Ptuple l -> not (List.for_all is_basic_pattern l)
     | Pusual _ | Prel _ | Pwild -> false
   in
-  array_exists (function (_,pat,_) -> deep pat) br
+  Array.exists (function (_,pat,_) -> deep pat) br
 
 let is_regular_match br =
   if Array.length br = 0 then false (* empty match becomes MLexn *)
@@ -543,7 +543,7 @@ let is_regular_match br =
 	| ConstructRef (ind,_) -> ind
 	| _ -> raise Impossible
       in
-      array_for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br
+      Array.for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br
     with Impossible -> false
 
 (*S Operations concerning lambdas. *)
@@ -770,7 +770,7 @@ let is_opt_pat (_,p,_) = match p with
   | _ -> false
 
 let factor_branches o typ br =
-  if array_exists is_opt_pat br then None (* already optimized *)
+  if Array.exists is_opt_pat br then None (* already optimized *)
   else begin
     census_clean ();
     for i = 0 to Array.length br - 1 do
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 8659de03e..9247baba2 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -270,7 +270,7 @@ let rec optim_se top to_appear s = function
 	else all := false
       done;
       if !all && top && not (library ())
-	&& (array_for_all (fun r -> not (List.mem r to_appear)) rv)
+	&& (Array.for_all (fun r -> not (List.mem r to_appear)) rv)
       then optim_se top to_appear s lse
       else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
   | (l,SEmodule m) :: lse ->
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 951049b7b..78126bc16 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -374,7 +374,7 @@ and pp_fix par env i (ids,bl) args =
 	  prvect_with_sep
       	    (fun () -> fnl () ++ str "and ")
 	    (fun (fi,ti) -> pr_id fi ++ pp_function env ti)
-	    (array_map2 (fun id b -> (id,b)) ids bl) ++
+	    (Array.map2 (fun id b -> (id,b)) ids bl) ++
 	  fnl () ++
 	  hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
 
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index ec338b1db..a0a59e73c 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -163,7 +163,7 @@ and pp_fix env j (ids,bl) args =
 	       (prvect_with_sep fnl
 		  (fun (fi,ti) ->
 		     paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
-		  (array_map2 (fun id b -> (id,b)) ids bl)) ++
+		  (Array.map2 (fun id b -> (id,b)) ids bl)) ++
 	     fnl () ++
       	     hov 2 (pp_apply (pr_id (ids.(j))) true args))))
 
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index f4cc397bc..d224f87df 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -95,7 +95,7 @@ let kind_of_formula gl term =
 			let is_trivial=
 			  let is_constant c =
 			    nb_prod c = mib.mind_nparams in
-			    array_exists is_constant mip.mind_nf_lc in
+			    Array.exists is_constant mip.mind_nf_lc in
 			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
 			    (has_realargs && not is_trivial)
 			  then
@@ -144,7 +144,7 @@ let build_atoms gl metagen side cciterm =
 	  let f l =
 	    List.fold_left_i g (1-(List.length l)) () l in
 	    if polarity && (* we have a constant constructor *)
-	      array_exists (function []->true|_->false) v
+	      Array.exists (function []->true|_->false) v
 	    then trivial:=true;
 	    Array.iter f v
       | Exists(i,l)->
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0796930fc..3505c4d9b 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -371,7 +371,7 @@ let is_property ptes_info t_x full_type_of_hyp =
   if isApp t_x
   then
     let pte,args = destApp t_x in
-    if isVar pte && array_for_all closed0 args
+    if isVar pte && Array.for_all closed0 args
     then
       try
 	let info = Idmap.find (destVar pte) ptes_info in
@@ -1415,11 +1415,11 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
       tclFIRST (List.map Equality.rewriteRL eqs )
     in
     let _,hrec_concl  = decompose_prod (pf_type_of gls (mkVar hrec)) in
-    let f_app = array_last (snd (destApp hrec_concl)) in
+    let f_app = Array.last (snd (destApp hrec_concl)) in
     let f =  (fst (destApp f_app)) in
     let rec backtrack : tactic =
       fun g ->
-	let f_app = array_last (snd (destApp (pf_concl g))) in
+	let f_app = Array.last (snd (destApp (pf_concl g))) in
 	match kind_of_term f_app with
 	  | App(f',_) when eq_constr f' f -> tclIDTAC g
 	  | _ -> tclTHEN rewrite backtrack g
@@ -1658,7 +1658,7 @@ let prove_principle_for_gen
       (* observe_tac "finish" *) (fun gl' ->
 	 let body =
 	   let _,args = destApp (pf_concl gl') in
-	   array_last args
+	   Array.last args
 	 in
 	 let body_info rec_hyps =
 	   {
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index f2eb4b23c..b97fc48f1 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -154,7 +154,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	    compute_new_princ_type_for_binder  remove mkLambda env x t b
 	| Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved
 	| App(f,args) when is_dom f ->
-	    let var_to_be_removed = destRel (array_last args) in
+	    let var_to_be_removed = destRel (Array.last args) in
 	    let num = get_fun_num f in
 	    raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement pre_princ num args))
 	| App(f,args) ->
@@ -479,7 +479,7 @@ let get_funs_constant mp dp =
 	let first_infos = extract_info true (List.hd l_bodies) in
 	let check body  = (* Hope this is correct *)
 	  let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) =
-	    ia1 = ia2 && na1 = na2 && array_equal eq_constr ta1 ta2 && array_equal eq_constr ca1 ca2
+	    ia1 = ia2 && na1 = na2 && Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2
 	  in
 	  if not (eq_infos first_infos (extract_info false body))
 	  then  error "Not a mutal recursive block"
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 1c2193449..490d52555 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1240,7 +1240,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b
     try
       List.iter_i
 	(fun i ((n,nt,is_defined) as param) ->
-	   if array_for_all
+	   if Array.for_all
 	     (fun l ->
 		let (n',nt',is_defined') = List.nth l i in
 		n = n' && Notation_ops.eq_glob_constr nt nt' && is_defined = is_defined')
@@ -1319,7 +1319,7 @@ let do_build_inductive
        Then save the graphs and reset Printing options to their primitive values
     *)
     let rel_arities = Array.mapi rel_arity funsargs in
-    Util.array_fold_left2 (fun env rel_name rel_ar ->
+    Util.Array.fold_left2 (fun env rel_name rel_ar ->
 			     Environ.push_named (rel_name,None, Constrintern.interp_constr Evd.empty env rel_ar) env) env relnames rel_arities
   in
   (* and of the real constructors*)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 1d1089a54..d8255e834 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -358,7 +358,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 			       | App(eq,args), App(graph',_)
 				   when
 				     (eq_constr eq eq_ind) &&
-				       array_exists  (eq_constr graph') graphs_constr ->
+				       Array.exists  (eq_constr graph') graphs_constr ->
 				   (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
 				    ::acc)
 			       | _ -> mkVar hid ::  acc
@@ -599,7 +599,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 			       | App(eq,args), App(graph',_)
 				   when
 				     (eq_constr eq eq_ind) &&
-				       array_exists  (eq_constr graph') graphs_constr ->
+				       Array.exists  (eq_constr graph') graphs_constr ->
 				   ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
 				    ::args.(2)::acc)
 			       | _ -> mkVar hid ::  acc
@@ -1029,7 +1029,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
   try
     let graphs_constr = Array.map mkInd graphs in
     let lemmas_types_infos =
-      Util.array_map2_i
+      Util.Array.map2_i
 	(fun i f_constr graph ->
 	   let const_of_f = destConst f_constr in
 	   let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
@@ -1056,7 +1056,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	       (fun entry ->
 		  (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type )
 	       )
-	       (make_scheme (array_map_to_list (fun const -> const,GType None) funs))
+	       (make_scheme (Array.map_to_list (fun const -> const,GType None) funs))
 	    )
     in
     let proving_tac =
@@ -1083,7 +1083,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
       )
       funs;
     let lemmas_types_infos =
-      Util.array_map2_i
+      Util.Array.map2_i
 	(fun i f_constr graph ->
 	   let const_of_f = destConst f_constr in
 	   let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
@@ -1169,7 +1169,7 @@ let revert_graph kn post_tac hid g =
 	    match info.completeness_lemma with
 	      | None -> tclIDTAC g
 	      | Some f_complete ->
-		  let f_args,res = array_chop (Array.length args - 1) args in
+		  let f_args,res = Array.chop (Array.length args - 1) args in
 		  tclTHENSEQ
 		    [
 		      h_generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 21c0d86a4..5915d3c0d 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -153,17 +153,9 @@ exception Found of int
 (* Array scanning *)
 
 let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int =
-  try
-    for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done;
-    Array.length arr (* all elt are positive *)
-  with Found i -> i
-
-let array_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b array): 'a =
-  let i = ref 0 in
-  Array.fold_left
-    (fun acc x ->
-      let res = f !i acc x in i := !i + 1; res)
-    acc arr
+match Array.find_i pred arr with
+| None -> Array.length arr (* all elt are positive *)
+| Some i -> i
 
 (* Like List.chop but except that [i] is the size of the suffix of [l]. *)
 let list_chop_end i l =
@@ -660,7 +652,7 @@ let rec merge_types shift accrec1
     returns the list of unlinked vars of [allargs2]. *)
 let build_link_map_aux (allargs1:identifier array) (allargs2:identifier array)
     (lnk:int merged_arg array) =
-  array_fold_lefti
+  Array.fold_left_i
     (fun i acc e ->
       if i = Array.length lnk - 1 then acc (* functional arg, not in allargs *)
       else
@@ -939,7 +931,7 @@ let merge (id1:identifier) (id2:identifier) (args1:identifier array)
                  as above: vars may be linked inside args2?? *)
     Array.mapi
       (fun i c ->
-        match array_find_i (fun i x -> x=c) args1 with
+        match Array.find_i (fun i x -> x=c) args1 with
           | Some j -> Linked j
           | None -> Unlinked)
       args2 in
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 8dbb75cdc..311ab3081 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -211,7 +211,7 @@ let compute_rhs bodyi index_of_f =
   let rec aux c =
     match kind_of_term c with
       | App (j, args) when isRel j && destRel j = index_of_f (* recursive call *) ->
-          let i = destRel (array_last args) in
+          let i = destRel (Array.last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
           PApp (snd (pattern_of_constr Evd.empty f), Array.map aux args)
@@ -301,7 +301,7 @@ let rec closed_under cset t =
   (ConstrSet.mem t cset) or
   (match (kind_of_term t) with
      | Cast(c,_,_) -> closed_under cset c
-     | App(f,l) -> closed_under cset f && array_for_all (closed_under cset) l
+     | App(f,l) -> closed_under cset f && Array.for_all (closed_under cset) l
      | _ -> false)
 
 (*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete
@@ -362,7 +362,7 @@ let path_of_int n =
 let rec subterm gl (t : constr) (t' : constr) =
   (pf_conv_x gl t t') or
   (match (kind_of_term t) with
-     | App (f,args) -> array_exists (fun t -> subterm gl t t') args
+     | App (f,args) -> Array.exists (fun t -> subterm gl t t') args
      | Cast(t,_,_) -> (subterm gl t t')
      | _ -> false)
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index f838b56c6..abf142e79 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -65,7 +65,7 @@ let rec mk_clos_but f_map subs t =
 and mk_clos_app_but f_map subs f args n =
   if n >= Array.length args then mk_atom(mkApp(f, args))
   else
-    let fargs, args' = array_chop n args in
+    let fargs, args' = Array.chop n args in
     let f' = mkApp(f,fargs) in
     match f_map f' with
         Some map ->