Removing useless casts between arrays and lists.

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

1 files changed, 9 insertions, 2 deletions

diff --git a/kernel/vars.ml b/kernel/vars.ml
index 1469192b1..12c1529c8 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -131,8 +131,15 @@ let substkey = Profile.declare_profile "substn_many";;
 let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;;
 *)
 
-let substnl laml n =
-  substn_many (Array.map make_substituend (Array.of_list laml)) n
+let make_subst = function
+| [] -> [||]
+| hd :: tl ->
+  let subst = Array.make (1 + List.length tl) (make_substituend hd) in
+  let iteri i x = Array.unsafe_set subst (succ i) (make_substituend x) in
+  let () = CList.iteri iteri tl in
+  subst
+
+let substnl laml n = substn_many (make_subst laml) n
 let substl laml = substnl laml 0
 let subst1 lam = substl [lam]