Small optimizations in unification.

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

2 files changed, 18 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)
 
diff --git a/lib/cArray.mli b/lib/cArray.mli
index 6608c06d24..e0ec095f3e 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -125,6 +125,9 @@ sig
   (** Return [true] if every element of the array is unique (for default 
       equality). *)
 
+  val rev_of_list : 'a list -> 'a array
+  (** [rev_of_list l] is equivalent to [Array.of_list (List.rev l)]. *)
+
   val rev_to_list : 'a array -> 'a list
   (** [rev_to_list a] is equivalent to [List.rev (List.of_array a)]. *)