From 451ecf7eb4fbd8ffa2058cdb8bb57e0b25a70b59 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 18 Sep 2012 16:00:57 +0000
Subject: More cleaning in CArray...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15819 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/termops.ml | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f8cd3609ad..2585d44898 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -340,6 +340,17 @@ let fold_rec_types g (lna,typarray,_) e =
   let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> g assum e) e ctxt
 
+let map_left2 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 map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -370,11 +381,11 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
       mkCase (ci, p', c', Array.map_left (f l) bl)
   | Fix (ln,(lna,tl,bl as fx)) ->
       let l' = fold_rec_types g fx l in
-      let (tl',bl') = Array.map_left_pair (f l) tl (f l') bl in
+      let (tl', bl') = map_left2 (f l) tl (f l') bl in
       mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl as fx)) ->
       let l' = fold_rec_types g fx l in
-      let (tl',bl') = Array.map_left_pair (f l) tl (f l') bl in
+      let (tl', bl') = map_left2 (f l) tl (f l') bl in
       mkCoFix (ln,(lna,tl',bl'))
 
 (* strong *)
-- 
cgit v1.2.3