From e2579d9529becfa6ad38b7209b2b7edbb5ca5534 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 28 Aug 2006 09:04:44 +0000
Subject: 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
---
 lib/util.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'lib')

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