aboutsummaryrefslogtreecommitdiff
path: root/lib/util.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/util.ml')
-rw-r--r--lib/util.ml10
1 files changed, 8 insertions, 2 deletions
diff --git a/lib/util.ml b/lib/util.ml
index 66485d5a36..ee373120e2 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -123,8 +123,6 @@ module Stringmap = Map.Make(struct type t = string let compare = compare end)
(* Lists *)
-let list_add_set x l = if List.mem x l then l else x::l
-
let list_intersect l1 l2 =
List.filter (fun x -> List.mem x l2) l1
@@ -267,6 +265,14 @@ let rec list_remove_first a = function
| b::l -> b::list_remove_first a l
| [] -> raise Not_found
+let list_add_set x l = if List.mem x l then l else x::l
+
+let list_eq_set l1 l2 =
+ let rec aux l1 = function
+ | [] -> l1 = []
+ | a::l2 -> aux (list_remove_first a l1) l2 in
+ try aux l1 l2 with Not_found -> false
+
let list_for_all2eq f l1 l2 = try List.for_all2 f l1 l2 with Failure _ -> false
let list_map_i f =