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

5 files changed, 19 insertions, 27 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0796930fca..3505c4d9b8 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 f2eb4b23cf..b97fc48f1d 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 1c21934495..490d52555c 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 1d1089a549..d8255e8342 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 21c0d86a4f..5915d3c0d4 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