From 05b51f0e873da7f39dc52e85329752241be176f5 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 23 Oct 2013 20:25:26 +0000
Subject: Small optimizations in unification.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16918 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/cArray.ml | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'lib/cArray.ml')

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)
 
-- 
cgit v1.2.3