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

16 files changed, 83 insertions, 83 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 196f5a0e7e..0ece3496e1 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1016,7 +1016,7 @@ let rec ungeneralize n ng body =
         let sign2,p = decompose_prod_n_assum ng p in
         let p = prod_applist p [mkRel (n+List.length sign+ng)] in
         it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in
-      mkCase (ci,p,c,array_map2 (fun q c ->
+      mkCase (ci,p,c,Array.map2 (fun q c ->
         let sign,b = decompose_lam_n_assum q c in
         it_mkLambda_or_LetIn (ungeneralize (n+q) ng b) sign)
         ci.ci_cstr_ndecls brs)
@@ -1046,7 +1046,7 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs =
         let pred = lift_predicate (-1) pred tomatch in
         let tomatch = relocate_index_tomatch 1 (n+1) tomatch in
         let tomatch = lift_tomatch_stack (-1) tomatch in
-        let brs = array_map2 (ungeneralize_branch n k) brs cs in
+        let brs = Array.map2 (ungeneralize_branch n k) brs cs in
         aux k brs tomatch pred tocheck deps
   | _ -> assert false
   in aux 0 brs tomatch pred tocheck deps
@@ -1255,7 +1255,7 @@ and match_current pb tomatch =
 	  let pb,deps = generalize_problem (names,dep) pb deps in
 
 	  (* We compile branches *)
-	  let brvals = array_map2 (compile_branch current realargs (names,dep) deps pb arsign) eqns cstrs in
+	  let brvals = Array.map2 (compile_branch current realargs (names,dep) deps pb arsign) eqns cstrs in
 	  (* We build the (elementary) case analysis *)
           let depstocheck = current::binding_vars_of_inductive typ in
           let brvals,tomatch,pred,inst =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d30c1a11fa..da5ccc96b3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -350,8 +350,8 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
   | IfStyle when aliastyp = None ->
       let bl' = Array.map detype bl in
       let nondepbrs =
-	array_map3 (extract_nondep_branches testdep) bl bl' consnargsl in
-      if array_for_all ((<>) None) nondepbrs then
+	Array.map3 (extract_nondep_branches testdep) bl bl' consnargsl in
+      if Array.for_all ((<>) None) nondepbrs then
 	GIf (dl,tomatch,(alias,pred),
              Option.get nondepbrs.(0),Option.get nondepbrs.(1))
       else
@@ -405,7 +405,7 @@ let rec detype (isgoal:bool) avoid env t =
     | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c
     | App (f,args) ->
 	GApp (dl,detype isgoal avoid env f,
-              array_map_to_list (detype isgoal avoid env) args)
+              Array.map_to_list (detype isgoal avoid env) args)
     | Const sp -> GRef (dl, ConstRef sp)
     | Evar (ev,cl) ->
         GEvar (dl, ev,
@@ -433,7 +433,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) =
 	 (id::avoid, add_name (Name id) env, id::l))
       (avoid, env, []) names in
   let n = Array.length tys in
-  let v = array_map3
+  let v = Array.map3
     (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t))
     bodies tys vn in
   GRec(dl,GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
@@ -449,7 +449,7 @@ and detype_cofix isgoal avoid env n (names,tys,bodies) =
 	 (id::avoid, add_name (Name id) env, id::l))
       (avoid, env, []) names in
   let ntys = Array.length tys in
-  let v = array_map2
+  let v = Array.map2
     (fun c t -> share_names isgoal 0 [] def_avoid def_env c (lift ntys t))
     bodies tys in
   GRec(dl,GCoFix n,Array.of_list (List.rev lfi),
@@ -501,7 +501,7 @@ and detype_eqns isgoal avoid env ci computable constructs consnargsl bl =
       mat
   with _ ->
     Array.to_list
-      (array_map3 (detype_eqn isgoal avoid env) constructs consnargsl bl)
+      (Array.map3 (detype_eqn isgoal avoid env) constructs consnargsl bl)
 
 and detype_eqn isgoal avoid env constr construct_nargs branch =
   let make_pat x avoid env b ids =
@@ -653,9 +653,9 @@ let rec subst_glob_constr subst raw =
           GIf (loc,c',(na,po'),b1',b2')
 
   | GRec (loc,fix,ida,bl,ra1,ra2) ->
-      let ra1' = array_smartmap (subst_glob_constr subst) ra1
-      and ra2' = array_smartmap (subst_glob_constr subst) ra2 in
-      let bl' = array_smartmap
+      let ra1' = Array.smartmap (subst_glob_constr subst) ra1
+      and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in
+      let bl' = Array.smartmap
         (List.smartmap (fun (na,k,obd,ty as dcl) ->
           let ty' = subst_glob_constr subst ty in
           let obd' = Option.smartmap (subst_glob_constr subst) obd in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 9284e2c237..f931d723f1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -692,7 +692,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
 let second_order_matching_with_args ts env evd ev l t =
 (*
   let evd,ev = evar_absorb_arguments env evd ev l in
-  let argoccs = array_map_to_list (fun _ -> None) (snd ev) in
+  let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in
   second_order_matching ts env evd ev argoccs t
 *)
   (evd,false)
@@ -704,12 +704,12 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
   let (term2,l2 as appr2) = decompose_app t2 in
   match kind_of_term term1, kind_of_term term2 with
   | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = []
-      & array_for_all (fun a -> eq_constr a term2 or isEvar a) args1 ->
+      & Array.for_all (fun a -> eq_constr a term2 or isEvar a) args1 ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
       choose_less_dependent_instance evk1 evd term2 args1
   | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = []
-      & array_for_all (fun a -> eq_constr a term1 or isEvar a) args2 ->
+      & Array.for_all (fun a -> eq_constr a term1 or isEvar a) args2 ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
       choose_less_dependent_instance evk2 evd term1 args2
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 0243a57801..700b168ae1 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -381,7 +381,7 @@ let restrict_applied_evar evd (evk,argsv) filter candidates =
   | Some filter ->
       let evi = Evd.find evd evk in
       let subfilter = extract_subfilter (evar_filter evi) filter in
-      array_filter_with subfilter argsv in
+      Array.filter_with subfilter argsv in
   evd,(newevk,newargsv)
 
 (* Restrict an evar in the current evar_map *)
@@ -392,7 +392,7 @@ let restrict_evar evd evk filter candidates =
 let restrict_instance evd evk filter argsv =
   match filter with None -> argsv | Some filter ->
   let evi = Evd.find evd evk in
-  array_filter_with (extract_subfilter (evar_filter evi) filter) argsv
+  Array.filter_with (extract_subfilter (evar_filter evi) filter) argsv
 
 (* This assumes an evar with identity instance and generalizes it over only
    the De Bruijn part of the context *)
@@ -827,7 +827,7 @@ let make_projectable_subst aliases sigma evi args =
 	    | _ ->
 		(rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs))
 	| _ -> anomaly "Instance does not match its signature")
-      sign (array_rev_to_list args,Idmap.empty,Constrmap.empty) in
+      sign (Array.rev_to_list args,Idmap.empty,Constrmap.empty) in
   (full_subst,cstr_subst)
 
 let make_pure_subst evi args =
@@ -836,7 +836,7 @@ let make_pure_subst evi args =
       match args with
 	| a::rest -> (rest, (id,a)::l)
 	| _ -> anomaly "Instance does not match its signature")
-    (evar_filtered_context evi) (array_rev_to_list args,[]))
+    (evar_filtered_context evi) (Array.rev_to_list args,[]))
 
 (*------------------------------------*
  * operations on the evar constraints *
@@ -927,7 +927,7 @@ let find_projectable_constructor env evd cstr k args cstr_subst =
       List.filter (fun (args',id) ->
 	(* is_conv is maybe too strong (and source of useless computation) *)
 	(* (at least expansion of aliases is needed) *)
-	array_for_all2 (is_conv env evd) args args') l in
+	Array.for_all2 (is_conv env evd) args args') l in
     List.map snd l
   with Not_found ->
     []
@@ -1155,7 +1155,7 @@ let filter_of_projection = function Invertible _ -> true | _ -> false
 let invert_invertible_arg evd aliases k (evk,argsv) args' =
   let evi = Evd.find_undefined evd evk in
   let subst,_ = make_projectable_subst aliases evd evi argsv in
-  let projs = array_map_to_list (invert_arg evd aliases k evk subst) args' in
+  let projs = Array.map_to_list (invert_arg evd aliases k evk subst) args' in
   Array.of_list (extract_unique_projections projs)
 
 (* Redefines an evar with a smaller context (i.e. it may depend on less
@@ -1343,9 +1343,9 @@ let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t =
   let f,args = decompose_app_vect t in
   match kind_of_term f with
   | Construct (ind,_) ->
-      let params,_ = array_chop (Inductiveops.inductive_nparams ind) args in
-      array_for_all (is_constrainable_in k g) params
-  | Ind _ -> array_for_all (is_constrainable_in k g) args
+      let params,_ = Array.chop (Inductiveops.inductive_nparams ind) args in
+      Array.for_all (is_constrainable_in k g) params
+  | Ind _ -> Array.for_all (is_constrainable_in k g) args
   | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2
   | Evar (ev',_) -> ev' <> ev (*If ev' needed, one may also try to restrict it*)
   | Var id -> Idset.mem id fv_ids
@@ -1443,7 +1443,7 @@ let check_evar_instance evd evk1 body conv_algo =
  * depend on these args). *)
 
 let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 =
-  if array_equal eq_constr argsv1 argsv2 then evd else
+  if Array.equal eq_constr argsv1 argsv2 then evd else
   (* Filter and restrict if needed *)
   let untypedfilter =
     restrict_upon_filter evd evk
@@ -1549,7 +1549,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
             materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in
 	  let ts = expansions_of_var aliases t in
 	  let test c = isEvar c or List.mem c ts in
-	  let filter = array_map_to_list test argsv' in
+	  let filter = Array.map_to_list test argsv' in
           let filter = apply_subfilter (evar_filter (Evd.find_undefined evd evk)) filter in
 
           let filter = closure_of_filter evd evk' filter in
@@ -1952,7 +1952,7 @@ let define_evar_as_product evd (evk,args) =
   (* Quick way to compute the instantiation of evk with args *)
   let na,dom,rng = destProd prod in
   let evdom = mkEvar (fst (destEvar dom), args) in
-  let evrngargs = array_cons (mkRel 1) (Array.map (lift 1) args) in
+  let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
   let evrng =  mkEvar (fst (destEvar rng), evrngargs) in
   evd,mkProd (na, evdom, evrng)
 
@@ -1987,7 +1987,7 @@ let define_evar_as_lambda env evd (evk,args) =
   let evd,lam = define_pure_evar_as_lambda env evd evk in
   (* Quick way to compute the instantiation of evk with args *)
   let na,dom,body = destLambda lam in
-  let evbodyargs = array_cons (mkRel 1) (Array.map (lift 1) args) in
+  let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
   let evbody = mkEvar (fst (destEvar body), evbodyargs) in
   evd,mkLambda (na, dom, evbody)
 
@@ -1998,7 +1998,7 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function
       let evd,lam = define_pure_evar_as_lambda env evd evk in
       let _,_,body = destLambda lam in
       let evk = fst (destEvar body) in
-      evar_absorb_arguments env evd (evk, array_cons a args) l
+      evar_absorb_arguments env evd (evk, Array.cons a args) l
 
 (* Refining an evar to a sort *)
 
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index d20afaf403..09225b2f65 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -125,7 +125,7 @@ let occur_glob_constr id =
     | GIf (loc,c,rtntyp,b1,b2) ->
 	occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
     | GRec (loc,fk,idl,bl,tyl,bv) ->
-        not (array_for_all4 (fun fid bl ty bd ->
+        not (Array.for_all4 (fun fid bl ty bd ->
           let rec occur_fix = function
               [] -> not (occur ty) && (fid=id or not(occur bd))
             | (na,k,bbd,bty)::bl ->
@@ -192,7 +192,7 @@ let free_glob_vars  =
 	  let vs2 = vars bounded1 vs1 tyl.(i) in
 	  vars bounded1 vs2 bv.(i)
 	in
-	array_fold_left_i vars_fix vs idl
+	Array.fold_left_i vars_fix vs idl
     | GCast (loc,c,k) -> let v = vars bounded vs c in
 	(match k with CastConv t | CastVM t -> vars bounded v t | _ -> v)
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index f11fb46134..15255ea270 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -321,7 +321,7 @@ let mis_make_indrec env sigma listdepkind mib =
 		(fun f -> appvect (f, Termops.extended_rel_vect ndepar lnonparrec))
 		fi
 	      in
-		array_map3
+		Array.map3
 		  (make_rec_branch_arg env sigma
 		      (nparrec,depPvec,larsign))
                   vecfi constrs (dest_subterms recargsvec.(tyi))
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index a026f53d4e..4062117b0f 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -79,7 +79,7 @@ let mis_is_recursive_subset listind rarg =
 	  | Mrec (_,i) -> List.mem i listind
           | _ -> false) rvec
   in
-  array_exists one_is_rec (dest_subterms rarg)
+  Array.exists one_is_rec (dest_subterms rarg)
 
 let mis_is_recursive (ind,mib,mip) =
   mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1))
@@ -400,7 +400,7 @@ let set_pattern_names env ind brv =
         rel_context_length ((prod_assum c)) -
         mib.mind_nparams)
       mip.mind_nf_lc in
-  array_map2 (set_names env) arities brv
+  Array.map2 (set_names env) arities brv
 
 let type_case_branches_with_names env indspec p c =
   let (ind,args) = indspec in
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 37cbcc0629..217398a6da 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -183,14 +183,14 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
       | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app ->
           let p = Array.length args2 - Array.length args1 in
           if p>=0 then
-            let args21, args22 = array_chop p args2 in
+            let args21, args22 = Array.chop p args2 in
 	    let c = mkApp(c2,args21) in
             let subst = merge_binding allow_bound_rels stk n c subst in
-            array_fold_left2 (sorec stk) subst args1 args22
+            Array.fold_left2 (sorec stk) subst args1 args22
           else raise PatternMatchingFailure
 
       | PApp (c1,arg1), App (c2,arg2) ->
-        (try array_fold_left2 (sorec stk) (sorec stk subst c1 c2) arg1 arg2
+        (try Array.fold_left2 (sorec stk) (sorec stk subst c1 c2) arg1 arg2
          with Invalid_argument _ -> raise PatternMatchingFailure)
 
       | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
@@ -292,7 +292,7 @@ let sub_match ?(partial_app=false) ?(closed=true) pat c =
             let mk_ctx = function
               | [app';c] -> mk_ctx (mkApp (app',[|c|]))
               | _ -> assert false in
-	    try_aux [app;array_last lc] mk_ctx next
+	    try_aux [app;Array.last lc] mk_ctx next
           else
             let rec aux2 app args next =
               match args with
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index e4ae1e4b85..1f16385a62 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -23,7 +23,7 @@ open Evd
 
 let rec occur_meta_pattern = function
   | PApp (f,args) ->
-      (occur_meta_pattern f) or (array_exists occur_meta_pattern args)
+      (occur_meta_pattern f) or (Array.exists occur_meta_pattern args)
   | PLambda (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
   | PProd (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
   | PLetIn (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
@@ -179,7 +179,7 @@ let rec subst_pattern subst pat =
   | PRel _ -> pat
   | PApp (f,args) ->
       let f' = subst_pattern subst f in
-      let args' = array_smartmap (subst_pattern subst) args in
+      let args' = Array.smartmap (subst_pattern subst) args in
 	if f' == f && args' == args then pat else
 	  PApp (f',args')
   | PSoApp (i,args) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0eff92b617..ed65cc9ea6 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -316,12 +316,12 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 	      type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
       let ctxtv = Array.map (type_bl env empty_rel_context) bl in
       let larj =
-        array_map2
+        Array.map2
           (fun e ar ->
              pretype_type empty_valcon (push_rel_context e env) evdref lvar ar)
           ctxtv lar in
       let lara = Array.map (fun a -> a.utj_val) larj in
-      let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
+      let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
       let nbfix = Array.length lar in
       let names = Array.map (fun id -> Name id) names in
       let _ = 
@@ -336,7 +336,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 	(* Note: bodies are not used by push_rec_types, so [||] is safe *)
       let newenv = push_rec_types (names,ftys,[||]) env in
       let vdefj =
-	array_map2_i
+	Array.map2_i
 	  (fun i ctxt def ->
              (* we lift nbfix times the type in tycon, because of
 	      * the nbfix variables pushed to newenv *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index fd9a312fc4..f20c0dd83a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -315,7 +315,7 @@ let rec whd_state_gen flags ts env sigma =
                     | App (f,cl) ->
 			let napp = Array.length cl in
 			if napp > 0 then
-			  let x', l' = whrec' (array_last cl, empty_stack) in
+			  let x', l' = whrec' (Array.last cl, empty_stack) in
                           match kind_of_term x' with
                             | Rel 1 when l' = empty_stack ->
 				let lc = Array.sub cl 0 (napp-1) in
@@ -371,7 +371,7 @@ let local_whd_state_gen flags sigma =
                     | App (f,cl) ->
 			let napp = Array.length cl in
 			if napp > 0 then
-			  let x', l' = whrec (array_last cl, empty_stack) in
+			  let x', l' = whrec (Array.last cl, empty_stack) in
                           match kind_of_term x' with
                             | Rel 1 when l' = empty_stack ->
 				let lc = Array.sub cl 0 (napp-1) in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b897c01afb..2a6dc35d14 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -176,8 +176,8 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
       (function d -> match kind_of_term d with
          | Rel k ->
              if
-	       array_for_all (noccurn k) tys
-	       && array_for_all (noccurn (k+nbfix)) bds
+	       Array.for_all (noccurn k) tys
+	       && Array.for_all (noccurn (k+nbfix)) bds
 	     then
 	       (k, List.nth labs (k-1))
 	     else
@@ -902,7 +902,7 @@ let contextually byhead (occs,c) f env sigma t =
       else if byhead then
 	(* find other occurrences of c in t; TODO: ensure left-to-right *)
         let (f,l) = destApp t in
-	mkApp (f, array_map_left (traverse envc) l)
+	mkApp (f, Array.map_left (traverse envc) l)
       else
 	t
     with PatternMatchingFailure ->
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 8e56d59a66..451dde11f3 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -127,11 +127,11 @@ struct
 	  | DApp (c1,t1), DApp (c2,t2)
 	  | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2
 	| DCase (ci,p1,c1,bl1),DCase (_,p2,c2,bl2) ->
-	    array_fold_left2 f (f (f acc p1 p2) c1 c2) bl1 bl2
+	    Array.fold_left2 f (f (f acc p1 p2) c1 c2) bl1 bl2
 	| DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) ->
-	    array_fold_left2 f (array_fold_left2 f acc ta1 ta2) ca1 ca2
+	    Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2
 	| DCoFix(i,ta1,ca1), DCoFix(_,ta2,ca2) ->
-	    array_fold_left2 f (array_fold_left2 f acc ta1 ta2) ca1 ca2
+	    Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2
 	| DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
 	    f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2
 	| _ -> assert false
@@ -147,11 +147,11 @@ struct
 	| DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2)
 	| DApp (t1,u1), DApp (t2,u2) -> DApp (f t1 t2,f u1 u2)
 	| DCase (ci,p1,c1,bl1), DCase (_,p2,c2,bl2) ->
-	    DCase (ci, f p1 p2, f c1 c2, array_map2 f bl1 bl2)
+	    DCase (ci, f p1 p2, f c1 c2, Array.map2 f bl1 bl2)
 	| DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) ->
-	    DFix (ia,i,array_map2 f ta1 ta2,array_map2 f ca1 ca2)
+	    DFix (ia,i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2)
 	| DCoFix (i,ta1,ca1), DCoFix (_,ta2,ca2) ->
-	    DCoFix (i,array_map2 f ta1 ta2,array_map2 f ca1 ca2)
+	    DCoFix (i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2)
 	| DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
 	    DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2)
 	| _ -> assert false
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 765f1e4fa7..9db16baac0 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -207,7 +207,7 @@ let push_rels_assum assums =
 
 let push_named_rec_types (lna,typarray,_) env =
   let ctxt =
-    array_map2_i
+    Array.map2_i
       (fun i na t ->
 	 match na with
 	   | Name id -> (id, None, lift i t)
@@ -266,14 +266,14 @@ let rec strip_head_cast c = match kind_of_term c with
 let rec drop_extra_implicit_args c = match kind_of_term c with
   (* Removed trailing extra implicit arguments, what improves compatibility
      for constants with recently added maximal implicit arguments *)
-  | App (f,args) when isEvar (array_last args) ->
+  | App (f,args) when isEvar (Array.last args) ->
       drop_extra_implicit_args
-	(mkApp (f,fst (array_chop (Array.length args - 1) args)))
+	(mkApp (f,fst (Array.chop (Array.length args - 1) args)))
   | _ -> c
 
 (* Get the last arg of an application *)
 let last_arg c = match kind_of_term c with
-  | App (f,cl) -> array_last cl
+  | App (f,cl) -> Array.last cl
   | _ -> anomaly "last_arg"
 
 (* Get the last arg of an application *)
@@ -296,10 +296,10 @@ let adjust_app_array_size f1 l1 f2 l2 =
   let len1 = Array.length l1 and len2 = Array.length l2 in
   if len1 = len2 then (f1,l1,f2,l2)
   else if len1 < len2 then
-    let extras,restl2 = array_chop (len2-len1) l2 in
+    let extras,restl2 = Array.chop (len2-len1) l2 in
     (f1, l1, appvect (f2,extras), restl2)
   else
-    let extras,restl1 = array_chop (len1-len2) l1 in
+    let extras,restl1 = Array.chop (len1-len2) l1 in
     (appvect (f1,extras), restl1, f2, l2)
 
 (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
@@ -336,7 +336,7 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
    (co-)fixpoint) *)
 
 let fold_rec_types g (lna,typarray,_) e =
-  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 -> g assum e) e ctxt
 
 
@@ -361,19 +361,19 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
       let a = al.(Array.length al - 1) in
       let hd = f l (mkApp (c, Array.sub al 0 (Array.length al - 1))) in
       mkApp (hd, [| f l a |])
-  | Evar (e,al) -> mkEvar (e, array_map_left (f l) al)
+  | Evar (e,al) -> mkEvar (e, Array.map_left (f l) al)
   | Case (ci,p,c,bl) ->
       (* In v8 concrete syntax, predicate is after the term to match! *)
       let c' = f l c in
       let p' = f l p in
-      mkCase (ci, p', c', array_map_left (f l) bl)
+      mkCase (ci, p', c', Array.map_left (f l) bl)
   | Fix (ln,(lna,tl,bl as fx)) ->
       let l' = fold_rec_types g fx l in
-      let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in
+      let (tl',bl') = Array.map_left_pair (f l) tl (f l') bl in
       mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl as fx)) ->
       let l' = fold_rec_types g fx l in
-      let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in
+      let (tl',bl') = Array.map_left_pair (f l) tl (f l') bl in
       mkCoFix (ln,(lna,tl',bl'))
 
 (* strong *)
@@ -400,30 +400,30 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
   | App (c,al) ->
       let c' = f l c in
       let al' = Array.map (f l) al in
-      if c==c' && array_for_all2 (==) al al' then cstr else mkApp (c', al')
+      if c==c' && Array.for_all2 (==) al al' then cstr else mkApp (c', al')
   | Evar (e,al) ->
       let al' = Array.map (f l) al in
-      if array_for_all2 (==) al al' then cstr else mkEvar (e, al')
+      if Array.for_all2 (==) al al' then cstr else mkEvar (e, al')
   | Case (ci,p,c,bl) ->
       let p' = f l p in
       let c' = f l c in
       let bl' = Array.map (f l) bl in
-      if p==p' && c==c' && array_for_all2 (==) bl bl' then cstr else
+      if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else
         mkCase (ci, p', c', bl')
   | Fix (ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
       let bl' = Array.map (f l') bl in
-      if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl'
+      if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
       else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
       let bl' = Array.map (f l') bl in
-      if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl'
+      if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
       else mkCoFix (ln,(lna,tl',bl'))
 
@@ -446,11 +446,11 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(lna,tl,bl)) ->
       let n' = iterate g (Array.length tl) n in
-      let fd = array_map2 (fun t b -> (t,b)) tl bl in
+      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
   | CoFix (_,(lna,tl,bl)) ->
       let n' = iterate g (Array.length tl) n in
-      let fd = array_map2 (fun t b -> (t,b)) tl bl in
+      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
 
 (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
@@ -469,11 +469,11 @@ let iter_constr_with_full_binders g f l c = match kind_of_term c with
   | Evar (_,args) -> Array.iter (f l) args
   | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl
   | Fix (_,(lna,tl,bl)) ->
-      let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
       Array.iter (f l) tl;
       Array.iter (f l') bl
   | CoFix (_,(lna,tl,bl)) ->
-      let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
       Array.iter (f l) tl;
       Array.iter (f l') bl
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7821a5f4f7..8955cc64c5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -71,7 +71,7 @@ let abstract_list_all env evd typ c l =
     error_cannot_find_well_typed_abstraction env evd p l
 
 let set_occurrences_of_last_arg args =
-  Some AllOccurrences :: List.tl (array_map_to_list (fun _ -> None) args)
+  Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args)
 
 let abstract_list_all_with_dependencies env evd typ c l =
   let evd,ev = new_evar evd env typ in
@@ -324,7 +324,7 @@ let use_metas_pattern_unification flags nb l =
   !global_evars_pattern_unification_flag && flags.use_pattern_unification
   || (Flags.version_less_or_equal Flags.V8_3 || 
       flags.use_meta_bound_pattern_unification) &&
-     array_for_all (fun c -> isRel c && destRel c <= nb) l
+     Array.for_all (fun c -> isRel c && destRel c <= nb) l
 
 let expand_key env = function
   | Some (ConstKey cst) -> constant_opt_value env cst
@@ -461,7 +461,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
             (try 
-	       array_fold_left2 (unirec_rec curenvnb CONV true wt)
+	       Array.fold_left2 (unirec_rec curenvnb CONV true wt)
 		 (unirec_rec curenvnb CONV true false
 		    (unirec_rec curenvnb CONV true false substn p1 p2) c1 c2)
                  cl1 cl2
@@ -503,7 +503,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
   and unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 =
     try
       let (f1,l1,f2,l2) = adjust_app_array_size f1 l1 f2 l2 in
-      array_fold_left2 (unirec_rec curenvnb CONV true false)
+      Array.fold_left2 (unirec_rec curenvnb CONV true false)
 	(unirec_rec curenvnb CONV true true substn f1 f2) l1 l2
     with ex when precatchable_exception ex ->
     try reduce curenvnb pb b false substn cM cN
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 00efa981d5..3213641405 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -182,7 +182,7 @@ and nf_stk env c t stk  =
       let (mind,_ as ind),allargs = find_rectype_a env t in
       let (mib,mip) = Inductive.lookup_mind_specif env ind in
       let nparams = mib.mind_nparams in
-      let params,realargs = Util.array_chop nparams allargs in
+      let params,realargs = Util.Array.chop nparams allargs in
       let pT =
 	hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in
       let pT = whd_betadeltaiota env pT in
@@ -264,7 +264,7 @@ and nf_fix env f =
   let ft = Array.map (fun v -> nf_val env v crazy_type) vt in
   let name = Array.init ndef (fun _ -> (Name (id_of_string "Ffix"))) in
   let env = push_rec_types (name,ft,ft) env in
-  let fb = Util.array_map2 (fun v t -> nf_fun env v t) vb ft in
+  let fb = Util.Array.map2 (fun v t -> nf_fun env v t) vb ft in
   mkFix ((rec_args,init),(name,ft,fb))
 
 and nf_fix_app env f vargs =
@@ -282,7 +282,7 @@ and nf_cofix env cf =
   let cft = Array.map (fun v -> nf_val env v crazy_type) vt in
   let name = Array.init ndef (fun _ -> (Name (id_of_string "Fcofix"))) in
   let env = push_rec_types (name,cft,cft) env in
-  let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in
+  let cfb = Util.Array.map2 (fun v t -> nf_val env v t) vb cft in
   mkCoFix (init,(name,cft,cfb))
 
 let cbv_vm env c t  =