# HG changeset patch
# User Matthias Görgens <matthias.goergens@xxxxxxxxxx>
# Date 1268698900 0
# Node ID dfc5d7edf140b39c0443409f332a11e7d876f0dd
# Parent  60c1e7bf1a307f6527e10db53c5ccc292e09c480
in stdext/Opt: Renamed cat_options to cat_some, to be more in line with the coming either module.

diff -r 60c1e7bf1a30 -r dfc5d7edf140 stdext/opt.ml
--- a/stdext/opt.ml
+++ b/stdext/opt.ml
@@ -53,7 +53,7 @@
 	| 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 -r 60c1e7bf1a30 -r dfc5d7edf140 stdext/opt.mli
--- a/stdext/opt.mli
+++ b/stdext/opt.mli
@@ -19,5 +19,5 @@
 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