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

3 files changed, 6 insertions, 7 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index f74240a23f..015141d84c 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 de7bdbb882..14154b6c88 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 26254be231..f1d44a9a53 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")