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

7 files changed, 17 insertions, 17 deletions

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))))