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

3 files changed, 6 insertions, 6 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)