Deplacement array_map_left and co dans Util

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5343 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 22 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f9e949c84..6680a2d0e 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -173,28 +173,6 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
    time being almost those of the ML representation (except for
    (co-)fixpoint) *)
 
-let array_map_left f a = (* Ocaml does not guarantee Array.map is LR *)
-  let l = Array.length a in (* (even if so), then we rewrite it *)
-  if l = 0 then [||] else begin
-    let r = Array.create l (f a.(0)) in
-    for i = 1 to l - 1 do
-      r.(i) <- f a.(i)
-    done;
-    r
-  end
-
-let array_map_left_pair f a g b =
-  let l = Array.length a in
-  if l = 0 then [||],[||] else begin
-    let r = Array.create l (f a.(0)) in
-    let s = Array.create l (g b.(0)) in
-    for i = 1 to l - 1 do
-      r.(i) <- f a.(i);
-      s.(i) <- g b.(i)
-    done;
-    r, s
-  end
-
 let fold_rec_types g (lna,typarray,_) e =
   let ctxt =
     array_map2_i