aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/termops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/termops.ml')
-rw-r--r--pretyping/termops.ml22
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