Renamed Option.Misc.compare to the more uniform Option.equal.

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

2 files changed, 13 insertions, 30 deletions

diff --git a/lib/option.ml b/lib/option.ml
index 9ed0bda870..02adc69478 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -23,6 +23,12 @@ 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
+
 exception IsNone
 
 (** [get x] returns [y] where [x] is [Some y]. It raises IsNone
@@ -165,20 +171,3 @@ module List =
 	 |x -> x
 
 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 faae301ab5..0b50c588b1 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -13,6 +13,8 @@
    they actually are similar considering ['a option] as a type
    of lists with at most one element. *)
 
+exception IsNone
+
 (** [has_some x] is [true] if [x] is of the form [Some y] and [false]
     otherwise.  *)
 val has_some : 'a option -> bool
@@ -20,7 +22,11 @@ val has_some : 'a option -> bool
 (** Negation of [has_some] *)
 val is_empty : 'a option -> bool
 
-exception IsNone
+(** [equal 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 both [Some _] then
+    [f] is called. Otherwise it returns [false]. *)
+val equal : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool
 
 (** [get x] returns [y] where [x] is [Some y]. It raises IsNone
     if [x] equals [None]. *)
@@ -106,15 +112,3 @@ module List : sig
 
   val find : ('a -> 'b option) -> 'a list -> 'b option
 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
-