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

10 files changed, 46 insertions, 46 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 210dbb02b..251c32ac5 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -499,7 +499,7 @@ and compact_vect s v k = compact_v [] s v k (Array.length v - 1)
 and compact_v acc s v k i =
   if i < 0 then
     let v' = Array.of_list acc in
-    if array_for_all2 (==) v v' then v,s else v',s
+    if Array.for_all2 (==) v v' then v,s else v',s
   else
     let (a',s') = compact_constr s v.(i) k in
     compact_v (a'::acc) s' v k (i-1)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index a2ce4f270..b8edcae72 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -325,10 +325,10 @@ let subst_mind_packet sub mbp =
   { mind_consnames = mbp.mind_consnames;
     mind_consnrealdecls = mbp.mind_consnrealdecls;
     mind_typename = mbp.mind_typename;
-    mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc;
+    mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
     mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
     mind_arity = subst_indarity sub mbp.mind_arity;
-    mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc;
+    mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
     mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
     mind_kelim = mbp.mind_kelim;
@@ -346,7 +346,7 @@ let subst_mind sub mib =
     mind_nparams_rec = mib.mind_nparams_rec;
     mind_params_ctxt =
       map_rel_context (subst_mps sub) mib.mind_params_ctxt;
-    mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
+    mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
     mind_constraints = mib.mind_constraints  }
 
 let hcons_indarity = function
@@ -360,13 +360,13 @@ let hcons_mind_packet oib =
    mind_typename = hcons_ident oib.mind_typename;
    mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
    mind_arity = hcons_indarity oib.mind_arity;
-   mind_consnames = array_smartmap hcons_ident oib.mind_consnames;
-   mind_user_lc = array_smartmap hcons_types oib.mind_user_lc;
-   mind_nf_lc = array_smartmap hcons_types oib.mind_nf_lc }
+   mind_consnames = Array.smartmap hcons_ident oib.mind_consnames;
+   mind_user_lc = Array.smartmap hcons_types oib.mind_user_lc;
+   mind_nf_lc = Array.smartmap hcons_types oib.mind_nf_lc }
 
 let hcons_mind mib =
   { mib with
-    mind_packets = array_smartmap hcons_mind_packet mib.mind_packets;
+    mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets;
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
     mind_constraints = hcons_constraints mib.mind_constraints }
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index f1adb5340..37a896c77 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -68,7 +68,7 @@ let push_rel = push_rel
 let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x
 
 let push_rec_types (lna,typarray,_) env =
-  let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
+  let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
 let fold_rel_context f env ~init =
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b93b9f19b..3199d0faa 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -253,7 +253,7 @@ let typecheck_inductive env mie =
   (* Compute/check the sorts of the inductive types *)
   let ind_min_levels = inductive_levels arities inds in
   let inds, cst =
-    array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst ->
+    Array.fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst ->
       let sign, s = dest_arity env full_arity in
       let status,cst = match s with
       | Type u when ar_level <> None (* Explicitly polymorphic *)
@@ -330,7 +330,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
   let largs = Array.of_list largs in
   if Array.length largs < nparams then
     raise (IllFormedInd (LocalNotEnoughArgs l));
-  let (lpar,largs') = array_chop nparams largs in
+  let (lpar,largs') = Array.chop nparams largs in
   let nhyps = List.length hyps in
   let rec check k index = function
     | [] -> ()
@@ -340,7 +340,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
 	  | Rel w when w = index -> check (k-1) (index+1) hyps
 	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
   in check (nparams-1) (n-nhyps) hyps;
-  if not (array_for_all (noccur_between n ntypes) largs') then
+  if not (Array.for_all (noccur_between n ntypes) largs') then
     failwith_non_pos_vect n ntypes largs'
 
 (* Computes the maximum number of recursive parameters :
@@ -518,7 +518,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
     in check_constr_rec ienv nmr [] c
   in
   let irecargs_nmr =
-    array_map2
+    Array.map2
       (fun id c ->
         let _,rawc = mind_extract_params lparams c in
           try
@@ -646,7 +646,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
 	mind_nb_args = !nblock;
 	mind_reloc_tbl = rtbl;
       } in
-  let packets = array_map2 build_one_packet inds recargs in
+  let packets = Array.map2 build_one_packet inds recargs in
     (* Build the mutual inductive *)
     { mind_record = isrecord;
       mind_ntypes = ntypes;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d86abb435..81e6c8f17 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -779,7 +779,7 @@ let check_one_fix renv recpos def =
   check_rec_call renv [] def
 
 let judgment_of_fixpoint (_, types, bodies) =
-  array_map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies
+  Array.map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies
 
 let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   let nbfix = Array.length bodies in
@@ -815,7 +815,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
         | _ -> raise_err env i NotEnoughAbstractionInFixBody in
     check_occur fixenv 1 def in
   (* Do it on every fixpoint *)
-  let rv = array_map2_i find_ind nvect bodies in
+  let rv = Array.map2_i find_ind nvect bodies in
   (Array.map fst rv, Array.map snd rv)
 
 
@@ -898,7 +898,7 @@ let check_one_cofix env nbfix def deftype =
             if (List.for_all (noccur_with_meta n nbfix) args)
             then
               let nbfix = Array.length vdefs in
-	      if (array_for_all (noccur_with_meta n nbfix) varit) then
+	      if (Array.for_all (noccur_with_meta n nbfix) varit) then
 		let env' = push_rec_types recdef env in
 		(Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs;
 		 List.iter (check_rec_call env alreadygrd n vlra) args)
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index e7a5227e0..61dc2bf29 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -339,7 +339,7 @@ let rec map_kn f f' c =
 	  in
 	  let p' = func p in
 	  let ct' = func ct in
-	  let l' = array_smartmap func l in
+	  let l' = Array.smartmap func l in
 	    if (ci.ci_ind==ci_ind && p'==p
 		&& l'==l && ct'==ct)then c
 	    else
@@ -368,21 +368,21 @@ let rec map_kn f f' c =
 	    else mkLetIn (na, b', t', ct')
       | App (ct,l) ->
 	  let ct' = func ct in
-	  let l' = array_smartmap func l in
+	  let l' = Array.smartmap func l in
 	    if (ct'== ct && l'==l) then c
 	    else mkApp (ct',l')
       | Evar (e,l) ->
-	  let l' = array_smartmap func l in
+	  let l' = Array.smartmap func l in
 	    if (l'==l) then c
 	    else mkEvar (e,l')
       | Fix (ln,(lna,tl,bl)) ->
-	  let tl' = array_smartmap func tl in
-	  let bl' = array_smartmap func bl in
+	  let tl' = Array.smartmap func tl in
+	  let bl' = Array.smartmap func bl in
 	    if (bl == bl'&& tl == tl') then c
 	    else mkFix (ln,(lna,tl',bl'))
       | CoFix(ln,(lna,tl,bl)) ->
-	  let tl' = array_smartmap func tl in
-	  let bl' = array_smartmap func bl in
+	  let tl' = Array.smartmap func tl in
+	  let bl' = Array.smartmap func bl in
 	    if (bl == bl'&& tl == tl') then c
 	    else mkCoFix (ln,(lna,tl',bl'))
       | _ -> c
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4ce3e7f22..76dcd1d3a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -153,7 +153,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
       | (z1::s1, z2::s2) ->
           let cu1 = cmp_rec s1 s2 cuniv in
           (match (z1,z2) with
-            | (Zlapp a1,Zlapp a2) -> array_fold_right2 f a1 a2 cu1
+            | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
                 let cu2 = f fx1 fx2 cu1 in
                 cmp_rec a1 a2 cu2
@@ -161,7 +161,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
                 if not (fmind ci1.ci_ind ci2.ci_ind) then
 		  raise NotConvertible;
 		let cu2 = f (l1,p1) (l2,p2) cu1 in
-                array_fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2
+                Array.fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2
             | _ -> assert false)
       | _ -> cuniv in
   if compare_stack_shape stk1 stk2 then
@@ -443,7 +443,7 @@ let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars
 let conv_leq ?(l2r=false) ?(evars=fun _->None) = fconv CUMUL l2r evars
 
 let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
-  array_fold_left2_i
+  Array.fold_left2_i
     (fun i c t1 t2 ->
       let c' =
         try conv_leq ~l2r ~evars env t1 t2
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index c590a5101..b8626e227 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -43,7 +43,7 @@ let add_mib_nameobjects mp l mib map =
   let add_mip_nameobjects j oib map =
     let ip = (ind,j) in
     let map =
-      array_fold_right_i
+      Array.fold_right_i
       (fun i id map ->
         Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map)
       oib.mind_consnames
@@ -51,7 +51,7 @@ let add_mib_nameobjects mp l mib map =
     in
       Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map
   in
-  array_fold_right_i add_mip_nameobjects mib.mind_packets map
+  Array.fold_right_i add_mip_nameobjects mib.mind_packets map
 
 
 (* creates (namedobject/namedmodule) map for the whole signature *)
@@ -154,7 +154,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
 	cst
   in
   let check_cons_types i cst p1 p2 =
-    array_fold_left3
+    Array.fold_left3
       (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst conv env t1 t2)
       cst
       p2.mind_consnames
@@ -203,11 +203,11 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   end;
   (* we first check simple things *)
   let cst =
-    array_fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets
+    Array.fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets
   in
   (* and constructor types in the end *)
   let cst =
-    array_fold_left2_i check_cons_types cst mib1.mind_packets mib2.mind_packets
+    Array.fold_left2_i check_cons_types cst mib1.mind_packets mib2.mind_packets
   in
     cst
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 07152d4b6..e54e56f12 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -463,10 +463,10 @@ let fold_constr f acc c = match kind_of_term c with
   | Evar (_,l) -> Array.fold_left f acc l
   | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
   | Fix (_,(lna,tl,bl)) ->
-      let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in
+      let fd = Array.map3 (fun na t b -> (na,t,b)) lna tl bl in
       Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd
   | CoFix (_,(lna,tl,bl)) ->
-      let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in
+      let fd = Array.map3 (fun na t b -> (na,t,b)) lna tl bl in
       Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd
 
 (* [iter_constr f c] iters [f] on the immediate subterms of [c]; it is
@@ -572,17 +572,17 @@ let compare_constr f t1 t2 =
   | _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast c2),l2))
   | App (c1,l1), App (c2,l2) ->
     Array.length l1 = Array.length l2 &&
-      f c1 c2 && array_for_all2 f l1 l2
-  | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
+      f c1 c2 && Array.for_all2 f l1 l2
+  | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & Array.for_all2 f l1 l2
   | Const c1, Const c2 -> eq_constant c1 c2
   | Ind c1, Ind c2 -> eq_ind c1 c2
   | Construct c1, Construct c2 -> eq_constructor c1 c2
   | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-      f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2
+      f p1 p2 & f c1 c2 & Array.for_all2 f bl1 bl2
   | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
-      ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2
+      ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-      ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2
+      ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2
   | _ -> false
 
 (*******************************)
@@ -618,9 +618,9 @@ let constr_ord_int f t1 t2 =
 	((f =? f) ==? f) b1 b2 t1 t2 c1 c2
     | App (c1,l1), _ when isCast c1 -> f (mkApp (pi1 (destCast c1),l1)) t2
     | _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast c2),l2))
-    | App (c1,l1), App (c2,l2) -> (f =? (array_compare f)) c1 c2 l1 l2
+    | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
     | Evar (e1,l1), Evar (e2,l2) ->
-	((-) =? (array_compare f)) e1 e2 l1 l2
+	((-) =? (Array.compare f)) e1 e2 l1 l2
     | Const c1, Const c2 -> kn_ord (canonical_con c1) (canonical_con c2)
     | Ind (spx, ix), Ind (spy, iy) ->
 	let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c
@@ -629,12 +629,12 @@ let constr_ord_int f t1 t2 =
 	  (let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c)
 	else c
     | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-	((f =? f) ==? (array_compare f)) p1 p2 c1 c2 bl1 bl2
+	((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2
     | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
-	((Pervasives.compare =? (array_compare f)) ==? (array_compare f))
+	((Pervasives.compare =? (Array.compare f)) ==? (Array.compare f))
 	ln1 ln2 tl1 tl2 bl1 bl2
     | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-	((Pervasives.compare =? (array_compare f)) ==? (array_compare f))
+	((Pervasives.compare =? (Array.compare f)) ==? (Array.compare f))
 	ln1 ln2 tl1 tl2 bl1 bl2
     | t1, t2 -> Pervasives.compare t1 t2
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 3ec08fef4..294d99eea 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -21,7 +21,7 @@ open Type_errors
 let conv_leq l2r = default_conv CUMUL ~l2r
 
 let conv_leq_vecti env v1 v2 =
-  array_fold_left2_i
+  Array.fold_left2_i
     (fun i c t1 t2 ->
       let c' =
         try default_conv CUMUL env t1 t2
@@ -476,7 +476,7 @@ and execute_recdef env (names,lar,vdef) i cu =
   univ_combinator cu2
     ((lara.(i),(names,lara,vdefv)),cst)
 
-and execute_array env = array_fold_map' (execute env)
+and execute_array env = Array.fold_map' (execute env)
 
 (* Derived functions *)
 let infer env constr =