From: Enrico Tassi Date: Tue, 15 Nov 2005 12:10:14 +0000 (+0000) Subject: list_uniq abstracted on equality X-Git-Tag: V_0_7_2_3~79 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=80269a92dc40205efaad3f5d49cd02b779fed285 list_uniq abstracted on equality --- diff --git a/helm/ocaml/extlib/hExtlib.ml b/helm/ocaml/extlib/hExtlib.ml index c66236e43..a76a5c76e 100644 --- a/helm/ocaml/extlib/hExtlib.ml +++ b/helm/ocaml/extlib/hExtlib.ml @@ -112,11 +112,11 @@ let is_alphanum c = is_alpha c || is_digit c (** {2 List processing} *) -let rec list_uniq = function +let rec list_uniq ?(eq=(=)) = function | [] -> [] | h::[] -> [h] - | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl) - | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl + | h1::h2::tl when eq h1 h2 -> list_uniq ~eq (h2 :: tl) + | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq ~eq tl let rec filter_map f = function diff --git a/helm/ocaml/extlib/hExtlib.mli b/helm/ocaml/extlib/hExtlib.mli index d12c042f5..40a1aca15 100644 --- a/helm/ocaml/extlib/hExtlib.mli +++ b/helm/ocaml/extlib/hExtlib.mli @@ -63,7 +63,8 @@ val trim_blanks: string -> string (** strip heading and trailing blanks *) (** {2 List processing} *) -val list_uniq: 'a list -> 'a list (** uniq unix filter on lists *) +val list_uniq: + ?eq:('a->'a->bool) -> 'a list -> 'a list (** uniq unix filter on lists *) val filter_map: ('a -> 'b option) -> 'a list -> 'b list (** filter + map *) val list_concat: ?sep:'a list -> 'a list list -> 'a list (**String.concat-like*)