Petite optimisation récursive-terminale en passant

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

1 files changed, 5 insertions, 3 deletions

diff --git a/lib/util.ml b/lib/util.ml
index cd7f09de33..08b85759a2 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -295,9 +295,11 @@ let list_try_find f =
   in 
   try_find_f
 
-let rec list_uniquize = function
-  | [] -> []
-  | h::t -> if List.mem h t then list_uniquize t else h::(list_uniquize t)
+let list_uniquize l =
+  let rec aux acc = function
+  | [] -> List.rev acc
+  | h::t -> if List.mem h acc then aux acc t else aux (h::acc) t
+  in aux [] l
 
 let rec list_distinct = function
   | h::t -> (not (List.mem h t)) && list_distinct t