From 847f28cb238c734cac9fb08aff00347d2eec7bb0 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 22 Jan 2009 18:56:39 +0000
Subject: Util.split_at : for quadratic to linear complexity

 This function is probably used only on small lists, but it's not a
 reason to let it be quadratic... I'm wondering how many other inefficient
 functions like this one may exist in the source of Coq.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11847 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index 93032140ce..c685ee2268 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -774,7 +774,7 @@ let list_split_at p =
   let rec split_at_loop x y = 
     match y with 
       | []      -> ([],[])
-      | (a::l)  -> if (p a) then (x,y) else (split_at_loop (x@[a]) l)
+      | (a::l)  -> if (p a) then (List.rev x,y) else split_at_loop (a::x) l
   in 
   split_at_loop []
 
-- 
cgit v1.2.3