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

4 files changed, 9 insertions, 13 deletions

diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 92b0d65365..dcac6eb799 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -77,7 +77,7 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
 let process_inductive sechyps modlist mib =
   let nparams = mib.mind_nparams in
   let inds =
-    array_map_to_list
+    Array.map_to_list
       (fun mip ->
 	 let arity = expmod_constr modlist (refresh_polymorphic_type_of_inductive (mib,mip)) in
 	 let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index f6b8ada428..bfd64778f2 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -157,7 +157,7 @@ let define_mutual_scheme_base kind suff f internal names mind =
   let ids = Array.init (Array.length mib.mind_packets) (fun i ->
       try List.assoc i names
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
-  let consts = array_map2 (define internal) ids cl in
+  let consts = Array.map2 (define internal) ids cl in
   declare_scheme kind (Array.mapi (fun i cst -> ((mind,i),cst)) consts);
   consts
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index a6677a78b0..e3c5142d9e 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -985,22 +985,18 @@ let admit_obligations n =
 
 exception Found of int
 
-let array_find f arr =
-  try Array.iteri (fun i x -> if f x then raise (Found i)) arr;
-    raise Not_found
-  with Found i -> i
-
 let next_obligation n tac =
   let prg = match n with
   | None -> get_any_prog_err ()
   | Some _ -> get_prog_err n
   in
   let obls, rem = prg.prg_obligations in
-  let i =
-    try array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = []) obls
-    with Not_found -> anomaly "Could not find a solvable obligation."
-  in solve_obligation prg i tac
-
+  let is_open _ x = x.obl_body = None && deps_remaining obls x.obl_deps = [] in
+  let i = match Array.find_i is_open obls with
+  | Some i -> i
+  | None -> anomaly "Could not find a solvable obligation."
+  in
+  solve_obligation prg i tac
 
 let init_program () =
   Coqlib.check_required_library ["Coq";"Init";"Datatypes"];
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index dc451fe050..c0b9b11101 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -171,7 +171,7 @@ let make_cases s =
 	let {Declarations.mind_nparams = np}
 	    , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr }
 	      = Global.lookup_inductive i in
-	Util.array_fold_right2
+	Util.Array.fold_right2
 	  (fun consname typ l ->
 	     let al = List.rev (fst (Term.decompose_prod typ)) in
 	     let al = Util.List.skipn np al in