avoid (Int.equal (cmp ...) 0) when a boolean equality exists

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

7 files changed, 11 insertions, 12 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index f74240a23..015141d84 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -586,7 +586,7 @@ type evaluable_global_reference =
 
 let eq_egr e1 e2 = match e1, e2 with
     EvalConstRef con1, EvalConstRef con2 -> eq_constant con1 con2
-  | EvalVarRef id1, EvalVarRef id2 -> Int.equal (Id.compare id1 id2) 0
+  | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2
   | _, _ -> false
 
 (** {6 Hash-consing of name objects } *)
diff --git a/kernel/term.ml b/kernel/term.ml
index de7bdbb88..14154b6c8 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -345,7 +345,7 @@ let isRelN n c = match kind_of_term c with Rel n' -> Int.equal n n' | _ -> false
 
 (* Tests if a variable *)
 let isVar c = match kind_of_term c with Var _ -> true | _ -> false
-let isVarId id c = match kind_of_term c with Var id' -> Int.equal (Id.compare id id') 0 | _ -> false
+let isVarId id c = match kind_of_term c with Var id' -> Id.equal id id' | _ -> false
 
 (* Tests if an inductive *)
 let isInd c = match kind_of_term c with Ind _ -> true | _ -> false
@@ -578,7 +578,7 @@ let compare_constr f t1 t2 =
   match kind_of_term t1, kind_of_term t2 with
   | Rel n1, Rel n2 -> Int.equal n1 n2
   | Meta m1, Meta m2 -> Int.equal m1 m2
-  | Var id1, Var id2 -> Int.equal (Id.compare id1 id2) 0
+  | Var id1, Var id2 -> Id.equal id1 id2
   | Sort s1, Sort s2 -> Int.equal (sorts_ord s1 s2) 0
   | Cast (c1,_,_), _ -> f c1 t2
   | _, Cast (c2,_,_) -> f t1 c2
@@ -849,7 +849,7 @@ let subst1_named_decl = subst1_decl
 let rec thin_val = function
   | [] -> []
   | (((id,{ sit = v }) as s)::tl) when isVar v ->
-      if Int.equal (Id.compare id (destVar v)) 0 then thin_val tl else s::(thin_val tl)
+      if Id.equal id (destVar v) then thin_val tl else s::(thin_val tl)
   | h::tl -> h::(thin_val tl)
 
 (* (replace_vars sigma M) applies substitution sigma to term M *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 26254be23..f1d44a9a5 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -58,7 +58,7 @@ module UniverseLevel = struct
   let equal u v = match u,v with
     | Set, Set -> true
     | Level (i1, dp1), Level (i2, dp2) ->
-      Int.equal i1 i2 && Int.equal (Names.DirPath.compare dp1 dp2) 0
+      Int.equal i1 i2 && Names.DirPath.equal dp1 dp2
     | _ -> false
 
   let make m n = Level (n, m)
@@ -908,8 +908,7 @@ let subst_large_constraints =
 let no_upper_constraints u cst =
   match u with
   | Atom u ->
-    let test (u1, _, _) =
-      not (Int.equal (UniverseLevel.compare u1 u) 0) in
+    let test (u1, _, _) = not (UniverseLevel.equal u1 u) in
     Constraint.for_all test cst
   | Max _ -> anomaly (Pp.str "no_upper_constraints")
 
diff --git a/library/lib.ml b/library/lib.ml
index baed92bd5..30beb653f 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -461,7 +461,7 @@ let section_segment_of_mutual_inductive kn =
 
 let rec list_mem_assoc x = function
   | [] -> raise Not_found
-  | (a, _) :: l -> Int.equal (Names.Id.compare a x) 0 || list_mem_assoc x l
+  | (a, _) :: l -> Names.Id.equal a x || list_mem_assoc x l
 
 let section_instance = function
   | VarRef id ->
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index e66458ebe..28c64c147 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -662,7 +662,7 @@ let is_self from e =
     | (ETName,ETName | ETReference, ETReference | ETBigint,ETBigint
       | ETPattern, ETPattern) -> true
     | ETOther(s1,s2), ETOther(s1',s2') ->
-      Int.equal (String.compare s1 s1') 0 && Int.equal (String.compare s2 s2') 0
+      String.equal s1 s1' && String.equal s2 s2'
     | _ -> false
 
 let is_binder_level from e =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 825a6adb7..5056c3123 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -221,7 +221,7 @@ let lookup_rel_id id sign =
     | []                     -> raise Not_found
     | (Anonymous, _, _) :: l -> lookrec (n + 1) l
     | (Name id', b, t) :: l  ->
-      if Int.equal (Names.Id.compare id' id) 0 then (n, b, t) else lookrec (n + 1) l
+      if Names.Id.equal id' id then (n, b, t) else lookrec (n + 1) l
   in
   lookrec 1 sign
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 55a8f5f80..0ef590cdf 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -259,7 +259,7 @@ let print_namespace ns =
         begin match match_dirpath ns dir with
         | Some [] as y -> y
         | Some (a::ns') ->
-            if Int.equal (Names.Id.compare a id) 0 then Some ns'
+            if Names.Id.equal a id then Some ns'
             else None
         | None -> None
         end
@@ -272,7 +272,7 @@ let print_namespace ns =
         begin match match_modulepath ns mp with
         | Some [] as y -> y
         | Some (a::ns') ->
-            if Int.equal (Names.Id.compare a id) 0 then Some ns'
+            if Names.Id.equal a id then Some ns'
             else None
         | None -> None
         end