# HG changeset patch # User Matthias Goergens # Date 1274191678 -3600 # Node ID 09ef44837b92567e54d946c7f3dbcad95a4bf126 # Parent abd16fd2af43edf2a81bd49c75e213bedb752a59 in stdext/Opt: Renamed cat_options to cat_some, to be more in line with the coming either module. Signed-off-by: Matthias Goergens diff --git a/stdext/opt.ml b/stdext/opt.ml --- a/stdext/opt.ml +++ b/stdext/opt.ml @@ -53,7 +53,7 @@ let fold_right f opt accu = | Some x -> f x accu | None -> accu -let cat_options a = List.map unbox (List.filter is_boxed a) +let cat_some a = List.map unbox (List.filter is_boxed a) let join = function | Some (Some a) -> Some a diff --git a/stdext/opt.mli b/stdext/opt.mli --- a/stdext/opt.mli +++ b/stdext/opt.mli @@ -19,5 +19,5 @@ val is_boxed : 'a option -> bool val to_list : 'a option -> 'a list val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b option -> 'a val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b -val cat_options : 'a option list -> 'a list +val cat_some : 'a option list -> 'a list val join : ('a option) option -> 'a option