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, 38 insertions, 37 deletions

diff --git a/checker/check.mllib b/checker/check.mllib
index b7e196d4b..d286651a1 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -8,6 +8,7 @@ Segmenttree
 Unicodetable
 Errors
 CList
+CArray
 Util
 Option
 Hashcons
diff --git a/checker/closure.ml b/checker/closure.ml
index c3351cea1..f86aa82eb 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -414,7 +414,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/checker/declarations.ml b/checker/declarations.ml
index ad14a3bbe..8b146d18b 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -268,7 +268,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
@@ -297,21 +297,21 @@ let rec map_kn f f' c =
 	    else LetIn (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 App (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 Evar (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 Fix (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 CoFix (ln,(lna,tl',bl'))
       | _ -> c
@@ -720,10 +720,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_arity 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;
@@ -742,7 +742,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  }
 
 (* Modules *)
diff --git a/checker/environ.ml b/checker/environ.ml
index d0b0b4ce9..a0fac3492 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -74,7 +74,7 @@ let push_rel d env =
 let push_rel_context ctxt x = 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
 
 (* Named context *)
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 6d936796a..3539289e7 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -127,7 +127,7 @@ let is_unit constrsinfos =
    | _ -> false
 
 let small_unit constrsinfos =
-  let issmall = array_for_all is_small_constr constrsinfos
+  let issmall = Array.for_all is_small_constr constrsinfos
   and isunit = is_unit constrsinfos in
   issmall, isunit
 
@@ -243,13 +243,13 @@ let typecheck_one_inductive env params mib mip =
   let _ = Array.map (infer_type env) mip.mind_user_lc in
   (* mind_nf_lc *)
   let _ = Array.map (infer_type env) mip.mind_nf_lc in
-  array_iter2 (conv env) mip.mind_nf_lc mip.mind_user_lc;
+  Array.iter2 (conv env) mip.mind_nf_lc mip.mind_user_lc;
   (* mind_consnrealdecls *)
   let check_cons_args c n =
     let ctx,_ = decompose_prod_assum c in
     if n <> rel_context_length ctx - rel_context_length params then
       failwith "bad number of real constructor arguments" in
-  array_iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls;
+  Array.iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls;
   (* mind_kelim: checked by positivity criterion ? *)
   let sorts =
     compute_elim_sorts env params mib mip.mind_arity mip.mind_nf_lc in
@@ -312,7 +312,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
     | [] -> ()
@@ -322,7 +322,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'
 
 (* Arguments of constructor: check the number of recursive parameters nrecp.
@@ -520,7 +520,7 @@ let check_positivity env_ar mind params nrecp inds =
   in
   let irecargs = Array.mapi check_one inds in
   let wfp = Rtree.mk_rec irecargs in
-  array_iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp
+  Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp
 
 (************************************************************************)
 (************************************************************************)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index f35d68ad1..605405e35 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -817,7 +817,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)
 
 
@@ -899,7 +899,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/checker/reduction.ml b/checker/reduction.ml
index 5243bb201..195f7d423 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -122,14 +122,14 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
       | (z1::s1, z2::s2) ->
           cmp_rec s1 s2;
           (match (z1,z2) with
-            | (Zlapp a1,Zlapp a2) -> array_iter2 f a1 a2
+            | (Zlapp a1,Zlapp a2) -> Array.iter2 f a1 a2
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
                 f fx1 fx2; cmp_rec a1 a2
             | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
                 if not (fmind ci1.ci_ind ci2.ci_ind) then
 		  raise NotConvertible;
 		f (l1,p1) (l2,p2);
-                array_iter2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2
+                Array.iter2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2
             | _ -> assert false)
       | _ -> () in
   if compare_stack_shape stk1 stk2 then
@@ -368,7 +368,7 @@ and convert_stacks univ infos lft1 lft2 stk1 stk2 =
     lft1 stk1 lft2 stk2
 
 and convert_vect univ infos lft1 lft2 v1 v2 =
-  array_iter2 (fun t1 t2 -> ccnv univ CONV infos lft1 lft2 t1 t2) v1 v2
+  Array.iter2 (fun t1 t2 -> ccnv univ CONV infos lft1 lft2 t1 t2) v1 v2
 
 let clos_fconv cv_pb env t1 t2 =
   let infos = create_clos_infos betaiotazeta env in
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 55ed06665..7d2ced7fd 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -42,7 +42,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
@@ -50,7 +50,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 *)
@@ -149,7 +149,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
         (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
   in
   let check_cons_types i p1 p2 =
-    array_iter2 (check_conv conv env)
+    Array.iter2 (check_conv conv env)
       (arities_of_specif kn (mib1,p1))
       (arities_of_specif kn (mib2,p2))
   in
@@ -194,9 +194,9 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     check (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
   end;
   (* we first check simple things *)
-  array_iter2 check_packet mib1.mind_packets mib2.mind_packets;
+  Array.iter2 check_packet mib1.mind_packets mib2.mind_packets;
   (* and constructor types in the end *)
-  let _ = array_map2_i check_cons_types mib1.mind_packets mib2.mind_packets
+  let _ = Array.map2_i check_cons_types mib1.mind_packets mib2.mind_packets
   in ()
 
 let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
diff --git a/checker/term.ml b/checker/term.ml
index a7fc0a8b8..b41bebca2 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -473,23 +473,23 @@ let compare_constr f t1 t2 =
   | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2
   | App (c1,l1), App (c2,l2) ->
       if Array.length l1 = Array.length l2 then
-        f c1 c2 & array_for_all2 f l1 l2
+        f c1 c2 & Array.for_all2 f l1 l2
       else
         let (h1,l1) = decompose_app t1 in
         let (h2,l2) = decompose_app t2 in
         if List.length l1 = List.length l2 then
           f h1 h2 & List.for_all2 f l1 l2
         else false
-  | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & 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_con_chk c1 c2
   | Ind c1, Ind c2 -> eq_ind_chk c1 c2
   | Construct (c1,i1), Construct (c2,i2) -> i1=i2 && eq_ind_chk 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
 
 let rec eq_constr m n =
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 03d2bedcf..91f58a04a 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -20,7 +20,7 @@ open Environ
 let inductive_of_constructor = fst
 
 let conv_leq_vecti env v1 v2 =
-  array_fold_left2_i
+  Array.fold_left2_i
     (fun i _ t1 t2 ->
       (try conv_leq env t1 t2
       with NotConvertible -> raise (NotConvertibleVect i)); ())
@@ -244,7 +244,7 @@ let type_fixpoint env lna lar lbody vdefj =
   try
     conv_leq_vecti env vdefj (Array.map (fun ty -> lift lt ty) lar)
   with NotConvertibleVect i ->
-    let vdefj = array_map2 (fun b ty -> b,ty) lbody vdefj in
+    let vdefj = Array.map2 (fun b ty -> b,ty) lbody vdefj in
     error_ill_typed_rec_body env i lna vdefj lar
 
 (************************************************************************)
@@ -293,7 +293,7 @@ let rec execute env cstr =
 		(* No sort-polymorphism *)
 		execute env f
 	in
-        let jl = array_map2 (fun c ty -> c,ty) args jl in
+        let jl = Array.map2 (fun c ty -> c,ty) args jl in
 	judge_of_apply env (f,j) jl
 
     | Lambda (name,c1,c2) ->
@@ -362,7 +362,7 @@ and execute_type env constr =
 
 and execute_recdef env (names,lar,vdef) i =
   let larj = execute_array env lar in
-  let larj = array_map2 (fun c ty -> c,ty) lar larj in
+  let larj = Array.map2 (fun c ty -> c,ty) lar larj in
   let lara = Array.map (assumption_of_judgment env) larj in
   let env1 = push_rec_types (names,lara,vdef) env in
   let vdefj = execute_array env1 vdef in