Useless array manipulation in Rtrees.

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

1 files changed, 5 insertions, 6 deletions

diff --git a/lib/rtree.ml b/lib/rtree.ml
index c016bf0c30..5806ebd000 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -41,21 +41,20 @@ let lift n t = if Int.equal n 0 then t else lift_rtree_rec 0 n t
 let rec subst_rtree_rec depth sub = function
     Param (i,j) as t ->
       if i < depth then t
-      else if i-depth < Array.length sub then
-        lift depth sub.(i-depth).(j)
-      else Param (i-Array.length sub,j)
+      else if i = depth then
+        lift depth (Rec (j, sub))
+      else Param (i - 1, j)
   | Node (l,sons) -> Node (l,Array.map (subst_rtree_rec depth sub) sons)
   | Rec(j,defs) ->
       Rec(j, Array.map (subst_rtree_rec (depth+1) sub) defs)
 
-let subst_rtree sub t = subst_rtree_rec 0 [|sub|] t
+let subst_rtree sub t = subst_rtree_rec 0 sub t
 
 (* To avoid looping, we must check that every body introduces a node
    or a parameter *)
 let rec expand = function
   | Rec(j,defs) ->
-      let sub = Array.init (Array.length defs) (fun i -> Rec(i,defs)) in
-      expand (subst_rtree sub defs.(j))
+      expand (subst_rtree defs defs.(j))
   | t -> t
 
 (* Given a vector of n bodies, builds the n mutual recursive trees.