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

4 files changed, 29 insertions, 6 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
diff --git a/lib/option.mli b/lib/option.mli
index 8e768d8af2..4047ebe1a2 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -98,3 +98,15 @@ module List : sig
       [Some y] (in the same order). *)
   val flatten : 'a option list -> 'a list
 end
+
+
+(** {6 Miscelaneous Primitives} *)
+
+module Misc : sig
+  (** [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]. *)
+   val compare : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool
+end
+
diff --git a/lib/util.ml b/lib/util.ml
index 99a203d52f..586365dd83 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -788,11 +788,6 @@ let interval n m =
   in 
   interval_n ([],m)
 
-let option_compare f a b = match (a,b) with
-  | None, None -> true
-  | Some a', Some b' -> f a' b'
-  | _ -> failwith "option_compare"
-
 
 let map_succeed f = 
   let rec map_f = function 
diff --git a/lib/util.mli b/lib/util.mli
index 331363f0ae..88b246a72b 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -223,7 +223,6 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list
 
 val interval : int -> int -> int list
 
-val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool 
 
 (* In [map_succeed f l] an element [a] is removed if [f a] raises *)
 (* [Failure _] otherwise behaves as [List.map f l] *)