1 files changed, 34 insertions, 16 deletions
diff --git a/lib/option.ml b/lib/option.ml
index d6df7063..9ea1a769 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -19,6 +19,26 @@ let has_some = function
   | None -> false
   | _ -> true
 
+let is_empty = function
+| None -> true
+| Some _ -> false
+
+(** Lifting equality onto option types. *)
+let equal f x y = match x, y with
+| None, None -> true
+| Some x, Some y -> f x y
+| _, _ -> false
+
+let compare f x y = match x, y with
+| None, None -> 0
+| Some x, Some y -> f x y
+| None, Some _ -> -1
+| Some _, None -> 1
+
+let hash f = function
+| None -> 0
+| Some x -> f x
+
 exception IsNone
 
 (** [get x] returns [y] where [x] is [Some y]. It raises IsNone
@@ -44,6 +64,14 @@ let flatten = function
   | _ -> None
 
 
+(** [append x y] is the first element of the concatenation of [x] and
+    [y] seen as lists. *)
+let append o1 o2 =
+  match o1 with
+  | Some _ -> o1
+  | None  -> o2
+
+
 (** {6 "Iterators"} ***)
 
 (** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing
@@ -153,21 +181,11 @@ module List =
   let rec flatten = function
     | x::l -> cons x (flatten l)
     | [] -> []
-end
-
 
+  let rec find f = function
+    |[] -> None
+    |h :: t -> match f h with
+	 |None -> find f t
+	 |x -> x
 
-(** {6 Miscelaneous Primitives} *)
-
-module Misc =
- struct
-  (** [Misc.compare f x y] lifts the equality predicate [f] to
-      option types. That is, if both [x] and [y] are [None] then
-      it returns [true], if they are bothe [Some _] then
-      [f] is called. Otherwise it returns [false]. *)
-   let compare f x y =
-     match x,y with
-     | None, None -> true
-     | Some z, Some w -> f z w
-     | _,_ -> false
 end