From cf7f9c5c71c2afcfac55391eab2f8059caa101fd Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 13 Feb 2004 17:53:28 +0000 Subject: 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 --- pretyping/termops.ml | 22 ---------------------- 1 file changed, 22 deletions(-) (limited to 'pretyping') 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 -- cgit v1.2.3