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, 16 insertions, 16 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0ce8a8aac4..d5f96e3fd6 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1015,7 +1015,7 @@ let any_any_branch =
 let rec glob_of_pat env = function
   | PRef ref -> GRef (loc,ref)
   | PVar id -> GVar (loc,id)
-  | PEvar (n,l) -> GEvar (loc,n,Some (array_map_to_list (glob_of_pat env) l))
+  | PEvar (n,l) -> GEvar (loc,n,Some (Array.map_to_list (glob_of_pat env) l))
   | PRel n ->
       let id = try match lookup_name_of_rel n env with
 	| Name id   -> id
@@ -1026,7 +1026,7 @@ let rec glob_of_pat env = function
   | PMeta None -> GHole (loc,Evar_kinds.InternalHole)
   | PMeta (Some n) -> GPatVar (loc,(false,n))
   | PApp (f,args) ->
-      GApp (loc,glob_of_pat env f,array_map_to_list (glob_of_pat env) args)
+      GApp (loc,glob_of_pat env f,Array.map_to_list (glob_of_pat env) args)
   | PSoApp (n,args) ->
       GApp (loc,GPatVar (loc,(true,n)),
         List.map (glob_of_pat env) args)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7ad1327fd8..a2be41700e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1307,7 +1307,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 		   intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r))
 	     in
 	       ((n, ro), List.rev rbl, intern_type env' ty, env')) dl in
-        let idl = array_map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
+        let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
 	     let env'' = List.fold_left_i (fun i en name -> 
 					     let (_,bli,tyi,_) = idl_temp.(i) in
 					     let fix_args = (List.map (fun (_,(na, bk, _, _)) -> (build_impls bk na)) bli) in
@@ -1334,7 +1334,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
               List.fold_left intern_local_binder (env,[]) bl in
             (List.rev rbl,
              intern_type env' ty,env')) dl in
-	let idl = array_map2 (fun (_,_,_,bd) (b,c,env') ->
+	let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') ->
 	     let env'' = List.fold_left_i (fun i en name ->
 					     let (bli,tyi,_) = idl_tmp.(i) in
 					     let cofix_args =  List.map (fun (_, (na, bk, _, _)) -> (build_impls bk na)) bli in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index c4cc38a568..64e890616f 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -176,7 +176,7 @@ let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty
 	  let vs2 = vars bound1 vs1 tyl.(i) in
 	  vars bound1 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 bound vs c in
 	(match k with CastConv t | CastVM t -> vars bound v t | _ -> v)
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 13356445f4..3429ab7b9a 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -97,10 +97,10 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
       let e',na = g e na in
       GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2)
   | NRec (fk,idl,dll,tl,bl) ->
-      let e,dll = array_fold_map (List.fold_map (fun e (na,oc,b) ->
+      let e,dll = Array.fold_map (List.fold_map (fun e (na,oc,b) ->
 	  let e,na = g e na in
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
-      let e',idl = array_fold_map (to_id g) e idl in
+      let e',idl = Array.fold_map (to_id g) e idl in
       GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
   | NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k)
   | NSort x -> GSort (loc,x)
@@ -423,12 +423,12 @@ let rec subst_notation_constr subst bound raw =
 
   | NRec (fk,idl,dll,tl,bl) ->
       let dll' =
-	array_smartmap (List.smartmap (fun (na,oc,b as x) ->
+	Array.smartmap (List.smartmap (fun (na,oc,b as x) ->
 	  let oc' =  Option.smartmap (subst_notation_constr subst bound) oc in
 	  let b' =  subst_notation_constr subst bound b in
 	  if oc' == oc && b' == b then x else (na,oc',b'))) dll in
-      let tl' = array_smartmap (subst_notation_constr subst bound) tl in
-      let bl' = array_smartmap (subst_notation_constr subst bound) bl in
+      let tl' = Array.smartmap (subst_notation_constr subst bound) tl in
+      let bl' = Array.smartmap (subst_notation_constr subst bound) bl in
       if dll' == dll && tl' == tl && bl' == bl then raw else
 	  NRec (fk,idl,dll',tl',bl')
 
@@ -500,7 +500,7 @@ let match_fix_kind fk1 fk2 =
   | GCoFix n1, GCoFix n2 -> n1 = n2
   | GFix (nl1,n1), GFix (nl2,n2) ->
       n1 = n2 &&
-      array_for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2
+      Array.for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2
   | _ -> false
 
 let match_opt f sigma t1 t2 = match (t1,t2) with
@@ -658,18 +658,18 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
       List.fold_left2 (match_in u alp metas) sigma [a1;b1;c1] [a2;b2;c2]
   | GRec (_,fk1,idl1,dll1,tl1,bl1), NRec (fk2,idl2,dll2,tl2,bl2)
       when match_fix_kind fk1 fk2 & Array.length idl1 =  Array.length idl2 &
-	array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2
+	Array.for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2
 	->
-      let alp,sigma = array_fold_left2
+      let alp,sigma = Array.fold_left2
 	(List.fold_left2 (fun (alp,sigma) (na1,_,oc1,b1) (na2,oc2,b2) ->
 	  let sigma =
 	    match_in u alp metas
               (match_opt (match_in u alp metas) sigma oc1 oc2) b1 b2
 	  in match_names metas (alp,sigma) na1 na2)) (alp,sigma) dll1 dll2 in
-      let sigma = array_fold_left2 (match_in u alp metas) sigma tl1 tl2 in
-      let alp,sigma = array_fold_right2 (fun id1 id2 alsig ->
+      let sigma = Array.fold_left2 (match_in u alp metas) sigma tl1 tl2 in
+      let alp,sigma = Array.fold_right2 (fun id1 id2 alsig ->
 	match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
-      array_fold_left2 (match_in u alp metas) sigma bl1 bl2
+      Array.fold_left2 (match_in u alp metas) sigma bl1 bl2
   | GCast(_,c1,CastConv t1), NCast (c2,CastConv t2)
   | GCast(_,c1,CastVM t1), NCast (c2,CastVM t2) ->
       match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2