Plus de combinateurs sont passés de Util à Option. Le module Options

devient Flags.




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 27 insertions, 0 deletions

diff --git a/lib/option.ml b/lib/option.ml
index 0ed36b0026..436358b555 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -32,6 +32,14 @@ let get = function
 (** [make x] returns [Some x]. *)
 let make x = Some x
 
+(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
+let init b x =
+  if b then 
+    Some x
+  else
+    None
+    
+
 (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
 let flatten = function
   | Some (Some y) -> Some y
@@ -120,3 +128,22 @@ let lift2 f x y =
   match x,y with
   | Some z, Some w -> Some (f z w)
   | _,_ -> None
+
+
+
+(** {6 Operations with Lists} *)
+
+module List =
+ struct 
+  (** [List.cons x l] equals [y::l] if [x] is [Some y] and [l] otherwise. *)
+  let cons x l =
+    match x with
+    | Some y -> y::l
+    | _ -> l
+ 
+  (** [List.flatten l] is the list of all the [y]s such that [l] contains
+      [Some y] (in the same order). *)
+  let rec flatten = function
+    | x::l -> cons x (flatten l)
+    | [] -> [] 
+end