Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.

4 files changed, 32 insertions, 32 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 08114abc4..435cf0a79 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -482,7 +482,7 @@ let rec lft_fconstr n ft =
 let lift_fconstr k f =
   if Int.equal k 0 then f else lft_fconstr k f
 let lift_fconstr_vect k v =
-  if Int.equal k 0 then v else CArray.Fun1.map lft_fconstr k v
+  if Int.equal k 0 then v else Array.Fun1.map lft_fconstr k v
 
 let clos_rel e i =
   match expand_rel i e with
@@ -547,7 +547,7 @@ let mk_clos_vect env v = match v with
 | [|v0; v1; v2|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2|]
 | [|v0; v1; v2; v3|] ->
   [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|]
-| v -> CArray.Fun1.map mk_clos env v
+| v -> Array.Fun1.map mk_clos env v
 
 (* Translate the head constructor of t from constr to fconstr. This
    function is parameterized by the function to apply on the direct
@@ -562,7 +562,7 @@ let mk_clos_deep clos_fun env t =
           term = FCast (clos_fun env a, k, clos_fun env b)}
     | App (f,v) ->
         { norm = Red;
-	  term = FApp (clos_fun env f, CArray.Fun1.map clos_fun env v) }
+          term = FApp (clos_fun env f, Array.Fun1.map clos_fun env v) }
     | Proj (p,c) ->
 	{ norm = Red;
 	  term = FProj (p, clos_fun env c) }
@@ -605,21 +605,21 @@ let rec to_constr constr_fun lfts v =
 		Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve)
     | FFix ((op,(lna,tys,bds)),e) ->
         let n = Array.length bds in
-        let ftys = CArray.Fun1.map mk_clos e tys in
-        let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in
+        let ftys = Array.Fun1.map mk_clos e tys in
+        let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in
 	let lfts' = el_liftn n lfts in
-	mkFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys,
-		         CArray.Fun1.map constr_fun lfts' fbds))
+        mkFix (op, (lna, Array.Fun1.map constr_fun lfts ftys,
+                         Array.Fun1.map constr_fun lfts' fbds))
     | FCoFix ((op,(lna,tys,bds)),e) ->
         let n = Array.length bds in
-        let ftys = CArray.Fun1.map mk_clos e tys in
-        let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in
+        let ftys = Array.Fun1.map mk_clos e tys in
+        let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in
 	let lfts' = el_liftn (Array.length bds) lfts in
-	mkCoFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys,
-		           CArray.Fun1.map constr_fun lfts' fbds))
+        mkCoFix (op, (lna, Array.Fun1.map constr_fun lfts ftys,
+                           Array.Fun1.map constr_fun lfts' fbds))
     | FApp (f,ve) ->
 	mkApp (constr_fun lfts f,
-	       CArray.Fun1.map constr_fun lfts ve)
+               Array.Fun1.map constr_fun lfts ve)
     | FProj (p,c) ->
         mkProj (p,constr_fun lfts c)
 
@@ -1024,14 +1024,14 @@ and norm_head info tab m =
       | FProd(na,dom,rng) ->
           mkProd(na, kl info tab dom, kl info tab rng)
       | FCoFix((n,(na,tys,bds)),e) ->
-          let ftys = CArray.Fun1.map mk_clos e tys in
+          let ftys = Array.Fun1.map mk_clos e tys in
           let fbds =
-            CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
+            Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
           mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
       | FFix((n,(na,tys,bds)),e) ->
-          let ftys = CArray.Fun1.map mk_clos e tys in
+          let ftys = Array.Fun1.map mk_clos e tys in
           let fbds =
-            CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
+            Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
           mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
       | FEvar((i,args),env) ->
           mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
diff --git a/kernel/constr.ml b/kernel/constr.ml
index a1779b36d..8f83d6baa 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -468,16 +468,16 @@ let iter_with_binders g f n c = match kind c with
   | Prod (_,t,c) -> f n t; f (g n) c
   | Lambda (_,t,c) -> f n t; f (g n) c
   | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
-  | App (c,l) -> f n c; CArray.Fun1.iter f n l
-  | Evar (_,l) -> CArray.Fun1.iter f n l
-  | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
+  | App (c,l) -> f n c; Array.Fun1.iter f n l
+  | Evar (_,l) -> Array.Fun1.iter f n l
+  | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
   | Proj (p,c) -> f n c
   | Fix (_,(_,tl,bl)) ->
-      CArray.Fun1.iter f n tl;
-      CArray.Fun1.iter f (iterate g (Array.length tl) n) bl
+      Array.Fun1.iter f n tl;
+      Array.Fun1.iter f (iterate g (Array.length tl) n) bl
   | CoFix (_,(_,tl,bl)) ->
-      CArray.Fun1.iter f n tl;
-      CArray.Fun1.iter f (iterate g (Array.length tl) n) bl
+      Array.Fun1.iter f n tl;
+      Array.Fun1.iter f (iterate g (Array.length tl) n) bl
 
 (* [map f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
@@ -625,7 +625,7 @@ let map_with_binders g f l c0 = match kind c0 with
     else mkLetIn (na, b', t', c')
   | App (c, al) ->
     let c' = f l c in
-    let al' = CArray.Fun1.Smart.map f l al in
+    let al' = Array.Fun1.Smart.map f l al in
     if c' == c && al' == al then c0
     else mkApp (c', al')
   | Proj (p, t) ->
@@ -633,25 +633,25 @@ let map_with_binders g f l c0 = match kind c0 with
     if t' == t then c0
     else mkProj (p, t')
   | Evar (e, al) ->
-    let al' = CArray.Fun1.Smart.map f l al in
+    let al' = Array.Fun1.Smart.map f l al in
     if al' == al then c0
     else mkEvar (e, al')
   | Case (ci, p, c, bl) ->
     let p' = f l p in
     let c' = f l c in
-    let bl' = CArray.Fun1.Smart.map f l bl in
+    let bl' = Array.Fun1.Smart.map f l bl in
     if p' == p && c' == c && bl' == bl then c0
     else mkCase (ci, p', c', bl')
   | Fix (ln, (lna, tl, bl)) ->
-    let tl' = CArray.Fun1.Smart.map f l tl in
+    let tl' = Array.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.Smart.map f l' bl in
+    let bl' = Array.Fun1.Smart.map f l' bl in
     if tl' == tl && bl' == bl then c0
     else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
-    let tl' = CArray.Fun1.Smart.map f l tl in
+    let tl' = Array.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.Smart.map f l' bl in
+    let bl' = Array.Fun1.Smart.map f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
 type instance_compare_fn = GlobRef.t -> int ->
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 91cc64523..4b8edf63f 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -140,7 +140,7 @@ let rec comp mk_cl s1 s2 =
     | ESID _, _ -> s2
     | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2)
     | _, CONS(x,s') ->
-        CONS(CArray.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s')
+        CONS(Array.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s')
     | CONS(x,s), SHIFT(k,s') ->
         let lg = Array.length x in
         if k == lg then comp mk_cl s s'
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 81fbd4f5e..38106fbf6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -84,7 +84,7 @@ let map_lift (l : lift) (v : fconstr array) = match v with
 | [|c0; c1|] -> [|(l, c0); (l, c1)|]
 | [|c0; c1; c2|] -> [|(l, c0); (l, c1); (l, c2)|]
 | [|c0; c1; c2; c3|] -> [|(l, c0); (l, c1); (l, c2); (l, c3)|]
-| v -> CArray.Fun1.map (fun l t -> (l, t)) l v
+| v -> Array.Fun1.map (fun l t -> (l, t)) l v
 
 let pure_stack lfts stk =
   let rec pure_rec lfts stk =