Small optimizations in unification.

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

1 files changed, 15 insertions, 0 deletions

diff --git a/lib/cArray.ml b/lib/cArray.ml
index e4b24d8fdc..5bbc813d55 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -83,6 +83,7 @@ sig
   val fold_map2' :
     ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
   val distinct : 'a array -> bool
+  val rev_of_list : 'a list -> 'a array
   val rev_to_list : 'a array -> 'a list
   val filter_with : bool list -> 'a array -> 'a array
 end
@@ -282,6 +283,20 @@ let fold_left_from n f a v =
   in
   fold a n
 
+let rev_of_list = function
+| [] -> [| |]
+| x :: l ->
+  let len = List.length l in
+  let ans = Array.make (succ len) x in
+  let rec set i = function
+  | [] -> ()
+  | x :: l ->
+    Array.unsafe_set ans i x;
+    set (pred i) l
+  in
+  let () = set (len - 1) l in
+  ans
+
 let map_to_list f v =
   List.map f (Array.to_list v)