Util.option_compare devient Option.Misc.Compare et change un peu de type

( ('a -> 'b -> bool) -> 'a option -> 'b option -> bool devient la même 
chose mais avec 'a='b ) et de contenu pour avoir une sémantique plus 
claire.



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

1 files changed, 17 insertions, 0 deletions

diff --git a/lib/option.ml b/lib/option.ml
index 436358b555..5539058136 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -147,3 +147,20 @@ module List =
     | x::l -> cons x (flatten l)
     | [] -> [] 
 end
+
+
+
+(** {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