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

11 files changed, 28 insertions, 45 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 34651e2cf2..e237583d72 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -173,7 +173,7 @@ let rec check_same_pattern p1 p2 =
     | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) when eq_reference c1 c2 ->
         let () = List.iter2 check_same_pattern a1 a2 in
         List.iter2 check_same_pattern b1 b2
-    | CPatAtom(_,r1), CPatAtom(_,r2) when Option.Misc.compare eq_reference r1 r2 -> ()
+    | CPatAtom(_,r1), CPatAtom(_,r2) when Option.equal eq_reference r1 r2 -> ()
     | CPatPrim(_,i1), CPatPrim(_,i2) when prim_token_eq i1 i2 -> ()
     | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when String.equal s1 s2 ->
         check_same_pattern e1 e2
@@ -185,7 +185,7 @@ let check_same_ref r1 r2 =
 let eq_located f (_, x) (_, y) = f x y
 
 let same_id (id1, c1) (id2, c2) =
-  Option.Misc.compare (eq_located id_eq) id1 id2 && Pervasives.(=) c1 c2
+  Option.equal (eq_located id_eq) id1 id2 && Pervasives.(=) c1 c2
 
 let rec check_same_type ty1 ty2 =
   match ty1, ty2 with
@@ -213,14 +213,14 @@ let rec check_same_type ty1 ty2 =
   | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when name_eq na1 na2 ->
       check_same_type a1 a2;
       check_same_type b1 b2
-  | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) when Option.Misc.compare Int.equal proj1 proj2 ->
+  | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) when Option.equal Int.equal proj1 proj2 ->
       check_same_ref r1 r2;
       List.iter2 check_same_type al1 al2
   | CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) ->
       check_same_type e1 e2;
       let check_args (a1,e1) (a2,e2) =
         let eq_expl = eq_located Constrintern.explicitation_eq in
-        if not (Option.Misc.compare eq_expl e1 e2) then failwith "not same expl";
+        if not (Option.equal eq_expl e1 e2) then failwith "not same expl";
         check_same_type a1 a2
       in
       List.iter2 check_args al1 al2
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9ab4c64cda..f1316bbfac 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1190,7 +1190,7 @@ let intern_ind_pattern genv env pat =
 
 let explicitation_eq ex1 ex2 = match ex1, ex2 with
 | ExplByPos (i1, id1), ExplByPos (i2, id2) ->
-  Int.equal i1 i2 && Option.Misc.compare id_eq id1 id2
+  Int.equal i1 i2 && Option.equal id_eq id1 id2
 | ExplByName id1, ExplByName id2 ->
   id_eq id1 id2
 | _ -> false
diff --git a/interp/notation.ml b/interp/notation.ml
index 50a536eabf..8a01c59852 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -820,7 +820,7 @@ let locate_notation prglob ntn scope =
 	    pr_notation_info prglob df r ++ tbrk (1,2) ++
 	    (if String.equal sc default_scope then mt () else (str ": " ++ str sc)) ++
 	    tbrk (1,2) ++
-	    (if Option.Misc.compare String.equal (Some sc) scope then str "(default interpretation)" else mt ())
+	    (if Option.equal String.equal (Some sc) scope then str "(default interpretation)" else mt ())
 	    ++ fnl ()))
 	l) ntns)
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 2bce973f55..2ad39d189e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -685,10 +685,10 @@ let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty
 let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty
 
 let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-  id_eq i1 i2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
+  id_eq i1 i2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2
 
 let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) =
-  name_eq n1 n2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
+  name_eq n1 n2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2
 
 (***************************************************************************)
 (*     Type of local contexts (telescopes)                                 *)
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
-
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 0c21cb805c..8e4351deb0 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -23,8 +23,8 @@ open Evd
 
 let case_info_pattern_eq i1 i2 =
   i1.cip_style == i2.cip_style &&
-  Option.Misc.compare eq_ind i1.cip_ind i2.cip_ind &&
-  Option.Misc.compare Int.equal i1.cip_ind_args i2.cip_ind_args &&
+  Option.equal eq_ind i1.cip_ind i2.cip_ind &&
+  Option.equal Int.equal i1.cip_ind_args i2.cip_ind_args &&
   i1.cip_extensible == i2.cip_extensible
 
 let rec constr_pattern_eq p1 p2 = match p1, p2 with
@@ -45,7 +45,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) ->
   name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
 | PSort s1, PSort s2 -> glob_sort_eq s1 s2
-| PMeta m1, PMeta m2 -> Option.Misc.compare id_eq m1 m2
+| PMeta m1, PMeta m2 -> Option.equal id_eq m1 m2
 | PIf (t1, l1, r1), PIf (t2, l2, r2) ->
   constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
 | PCase (info1, p1, r1, l1), PCase (info2, p2, r2, l2) ->
diff --git a/proofs/goal.ml b/proofs/goal.ml
index c076cd676c..6b672d2cbb 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -385,7 +385,7 @@ let convert_hyp check (id,b,bt as d) env rdefs gl info =
     (fun _ (_,c,ct) _ ->
        if check && not (Reductionops.is_conv env sigma bt ct) then
 	 Errors.error ("Incorrect change of the type of "^(Names.string_of_id id));
-       if check && not (Option.Misc.compare (Reductionops.is_conv env sigma) b c) then
+       if check && not (Option.equal (Reductionops.is_conv env sigma) b c) then
 	 Errors.error ("Incorrect change of the body of "^(Names.string_of_id id));
        d)
   in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 725f16b8ef..b8341f1aad 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -472,7 +472,7 @@ let convert_hyp sign sigma (id,b,bt as d) =
         let env = Global.env_of_context sign in
         if !check && not (is_conv env sigma bt ct) then
 	  error ("Incorrect change of the type of "^(string_of_id id)^".");
-        if !check && not (Option.Misc.compare (is_conv env sigma) b c) then
+        if !check && not (Option.equal (is_conv env sigma) b c) then
 	  error ("Incorrect change of the body of "^(string_of_id id)^".");
        if !check then reorder := check_decl_position env sign d;
        d) in
diff --git a/tactics/auto.ml b/tactics/auto.ml
index a462460a5d..49841ecfab 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -117,7 +117,7 @@ type search_entry = stored_data list * stored_data list * Bounded_net.t
 let empty_se = ([],[],Bounded_net.create ())
 
 let eq_pri_auto_tactic (_, x) (_, y) =
-  if Int.equal x.pri y.pri && Option.Misc.compare constr_pattern_eq x.pat y.pat then
+  if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then
     match x.code,y.code with
       | Res_pf(cstr,_),Res_pf(cstr1,_) -> 
 	   eq_constr cstr cstr1
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e6ea72e747..53876134b9 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -892,7 +892,7 @@ let make_interpretation_type isrec = function
 
 let make_interpretation_vars recvars allvars =
   let eq_subscope (sc1, l1) (sc2, l2) =
-    Option.Misc.compare String.equal sc1 sc2 &&
+    Option.equal String.equal sc1 sc2 &&
     List.equal String.equal l1 l2
   in
   List.iter (fun (x,y) ->