aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lib/util.ml8
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