Monomorphized a lot of equalities over OCaml integers, thanks to

the new Int module. Only the most obvious were removed, so there
are a lot more in the wild.

This may sound heavyweight, but it has two advantages:

1. Monomorphization is explicit, hence we do not miss particular
optimizations of equality when doing it carelessly with the generic
equality.

2. When we have removed all the generic equalities on integers, we
will be able to write something like "let (=) = ()" to retrieve all
its other uses (mostly faulty) spread throughout the code, statically.

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

13 files changed, 90 insertions, 83 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 9e695e3d3..deba56f73 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -108,7 +108,7 @@ let empty_comp_env ()=
 (*i Creation functions for comp_env *)
 
 let rec add_param n sz l =
-  if n = 0 then l else add_param (n - 1) sz (n+sz::l)
+  if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l)
 
 let comp_env_fun arity =
   { nb_stack = arity;
@@ -280,14 +280,14 @@ let rec is_tailcall = function
 let rec add_pop n = function
   | Kpop m :: cont -> add_pop (n+m) cont
   | Kreturn m:: cont -> Kreturn (n+m) ::cont
-  | cont -> if n = 0 then cont else Kpop n :: cont
+  | cont -> if Int.equal n 0 then cont else Kpop n :: cont
 
 let add_grab arity lbl cont =
-  if arity = 1 then Klabel lbl :: cont
+  if Int.equal arity 1 then Klabel lbl :: cont
   else Krestart :: Klabel lbl :: Kgrab (arity - 1) :: cont
 
 let add_grabrec rec_arg arity lbl cont =
-  if arity = 1 then
+  if Int.equal arity 1 then
     Klabel lbl :: Kgrabrec 0 :: Krestart :: cont
   else
     Krestart :: Klabel lbl :: Kgrabrec rec_arg ::
@@ -331,7 +331,7 @@ let init_fun_code () = fun_code := []
 let code_construct tag nparams arity cont =
   let f_cont =
       add_pop nparams
-      (if arity = 0 then
+      (if Int.equal arity 0 then
 	[Kconst (Const_b0 tag); Kreturn 0]
        else [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0])
     in
@@ -397,7 +397,7 @@ let rec str_const c =
               with Not_found ->
 		(* 3/ if no special behavior is available, then the compiler
 		      falls back to the normal behavior *)
-		if arity = 0 then Bstrconst(Const_b0 num)
+		if Int.equal arity 0 then Bstrconst(Const_b0 num)
 		else
 		  let rargs = Array.sub args nparams arity in
 		  let b_args = Array.map str_const rargs in
@@ -435,7 +435,7 @@ let rec str_const c =
 	let oip = oib.mind_packets.(j) in
 	let num,arity = oip.mind_reloc_tbl.(i-1) in
 	let nparams = oib.mind_nparams in
-	if nparams + arity = 0 then Bstrconst(Const_b0 num)
+	if Int.equal (nparams + arity) 0 then Bstrconst(Const_b0 num)
 	else Bconstruct_app(num,nparams,arity,[||])
       end
   | _ -> Bconstr c
@@ -622,7 +622,7 @@ let rec compile_constr reloc c sz cont =
       (* Compiling regular constructor branches *)
       for i = 0 to Array.length tbl - 1 do
 	let tag, arity = tbl.(i) in
-	if arity = 0 then
+	if Int.equal arity 0 then
 	  let lbl_b,code_b =
 	    label_code(compile_constr reloc branchs.(i) sz_b (branch :: !c)) in
 	  lbl_consts.(tag) <- lbl_b;
@@ -669,7 +669,7 @@ and compile_str_cst reloc sc sz cont =
       let nargs = Array.length args in
       comp_args compile_str_cst reloc args sz (Kmakeblock(nargs,tag) :: cont)
   | Bconstruct_app(tag,nparams,arity,args) ->
-      if Array.length args = 0 then code_construct tag nparams arity cont
+      if Int.equal (Array.length args) 0 then code_construct tag nparams arity cont
       else
 	comp_app
 	  (fun _ _ _ cont -> code_construct tag nparams arity cont)
@@ -689,7 +689,7 @@ and compile_const =
     Retroknowledge.get_vm_compiling_info (!global_env).retroknowledge
                   (kind_of_term (mkConst kn)) reloc args sz cont
   with Not_found ->
-    if nargs = 0 then
+    if Int.equal nargs 0 then
       Kgetglobal (get_allias !global_env kn) :: cont
     else
       comp_app (fun _ _ _ cont ->
@@ -760,7 +760,7 @@ let compile_structured_int31 fc args =
 let dynamic_int31_compilation fc reloc args sz cont =
   if not fc then raise Not_found else
     let nargs = Array.length args in
-      if nargs = 31 then
+      if Int.equal nargs 31 then
 	let (escape,labeled_cont) = make_branch cont in
 	let else_lbl = Label.create() in
 	  comp_args compile_str_cst reloc args sz
@@ -778,7 +778,7 @@ let dynamic_int31_compilation fc reloc args sz cont =
 	    fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)];
 	    Kclosure(lbl,0) :: cont
 	in
-	  if nargs = 0 then
+	  if Int.equal nargs 0 then
 	    code_construct cont
 	  else
 	    comp_app (fun _ _ _ cont -> code_construct cont)
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 680a5f9f2..90b4f0ae0 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -165,7 +165,7 @@ let emit_instr = function
       then out(opENVACC1 + n - 1)
       else (out opENVACC; out_int n)
   | Koffsetclosure ofs ->
-      if ofs = -2 || ofs = 0 || ofs = 2
+      if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
       then out (opOFFSETCLOSURE0 + ofs / 2)
       else (out opOFFSETCLOSURE; out_int ofs)
   | Kpush ->
@@ -214,7 +214,7 @@ let emit_instr = function
   | Kconst c ->
       out opGETGLOBAL; slot_for_const c
   | Kmakeblock(n, t) ->
-      if n = 0 then raise (Invalid_argument "emit_instr : block size = 0")
+      if Int.equal n 0 then raise (Invalid_argument "emit_instr : block size = 0")
       else if n < 4 then (out(opMAKEBLOCK1 + n - 1); out_int t)
       else (out opMAKEBLOCK; out_int n; out_int t)
   | Kmakeprod ->
@@ -279,7 +279,7 @@ let rec emit = function
       else (out opPUSHENVACC; out_int n);
       emit c
   | Kpush :: Koffsetclosure ofs :: c ->
-      if ofs = -2 || ofs = 0 || ofs = 2
+      if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
       then out(opPUSHOFFSETCLOSURE0 + ofs / 2)
       else (out opPUSHOFFSETCLOSURE; out_int ofs);
       emit c
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 51e264106..681fb8533 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -354,7 +354,7 @@ and stack = stack_member list
 
 let empty_stack = []
 let append_stack v s =
-  if Array.length v = 0 then s else
+  if Int.equal (Array.length v) 0 then s else
   match s with
   | Zapp l :: s -> Zapp (Array.append v l) :: s
   | _ -> Zapp v :: s
@@ -398,7 +398,7 @@ let rec stack_assign s p c = match s with
          Zapp nargs :: s)
   | _ -> s
 let rec stack_tail p s =
-  if p = 0 then s else
+  if Int.equal p 0 then s else
     match s with
       | Zapp args :: s ->
 	  let q = Array.length args in
@@ -719,7 +719,7 @@ let get_nth_arg head n stk =
           let bef = Array.sub args 0 n in
           let aft = Array.sub args (n+1) (q-n-1) in
           let stk' =
-            List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in
+            List.rev (if Int.equal n 0 then rstk else (Zapp bef :: rstk)) in
           (Some (stk', args.(n)), append_stack aft s')
     | Zupdate(m)::s ->
         strip_rec rstk (update m (h.norm,h.term)) n s
@@ -764,7 +764,7 @@ let rec reloc_rargs_rec depth stk =
     | _ -> stk
 
 let reloc_rargs depth stk =
-  if depth = 0 then stk else reloc_rargs_rec depth stk
+  if Int.equal depth 0 then stk else reloc_rargs_rec depth stk
 
 let rec drop_parameters depth n argstk =
   match argstk with
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 37a896c77..301c3b152 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -423,7 +423,7 @@ let register =
     let nth_digit_plus_one i n = (* calculates the nth (starting with 0)
                                     digit of i and adds 1 to it
                                     (nth_digit_plus_one 1 3 = 2) *)
-      if (land) i ((lsl) 1 n) = 0 then
+      if Int.equal (i land (1 lsl n)) 0 then
         1
       else
         2
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 0bd7c515c..30c2387ea 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -29,14 +29,14 @@ let el_id = ELID
 let rec el_shft_rec n = function
   | ELSHFT(el,k) -> el_shft_rec (k+n) el
   | el           -> ELSHFT(el,n)
-let el_shft n el = if n = 0 then el else el_shft_rec n el
+let el_shft n el = if Int.equal n 0 then el else el_shft_rec n el
 
 (* cross n binders *)
 let rec el_liftn_rec n = function
   | ELID        -> ELID
   | ELLFT(k,el) -> el_liftn_rec (n+k) el
   | el          -> ELLFT(n, el)
-let el_liftn n el = if n = 0 then el else el_liftn_rec n el
+let el_liftn n el = if Int.equal n 0 then el else el_liftn_rec n el
 
 let el_lift el = el_liftn_rec 1 el
 
@@ -73,7 +73,7 @@ type 'a subs =
 
 let subs_id i = ESID i
 
-let subs_cons(x,s) = if Array.length x = 0 then s else CONS(x,s)
+let subs_cons(x,s) = if Int.equal (Array.length x) 0 then s else CONS(x,s)
 
 let subs_liftn n = function
   | ESID p        -> ESID (p+n) (* bounded identity lifted extends by p *)
@@ -81,13 +81,13 @@ let subs_liftn n = function
   | lenv          -> LIFT (n,lenv)
 
 let subs_lift a = subs_liftn 1 a
-let subs_liftn n a = if n = 0 then a else subs_liftn n a
+let subs_liftn n a = if Int.equal n 0 then a else subs_liftn n a
 
 let subs_shft = function
   | (0, s)            -> s
   | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1)
   | (n, s)            -> SHIFT (n,s)
-let subs_shft (n,a) = if n = 0 then a else subs_shft(n,a)
+let subs_shft (n,a) = if Int.equal n 0 then a else subs_shft(n,a)
 
 let subs_shift_cons = function
   (0, s, t)           -> CONS(t,s)
@@ -99,7 +99,7 @@ let rec is_subs_id = function
     ESID _     -> true
   | LIFT(_,s)  -> is_subs_id s
   | SHIFT(0,s) -> is_subs_id s
-  | CONS(x,s)  -> Array.length x = 0 && is_subs_id s
+  | CONS(x,s)  -> Int.equal (Array.length x) 0 && is_subs_id s
   | _          -> false
 
 (* Expands de Bruijn k in the explicit substitution subs
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 1c12c9e24..6b993604d 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -349,7 +349,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
     recursive parameters *)
 
 let compute_rec_par (env,n,_,_) hyps nmr largs =
-if nmr = 0 then 0 else
+if Int.equal nmr 0 then 0 else
 (* start from 0, hyps will be in reverse order *)
   let (lpar,_) = List.chop nmr largs in
   let rec find k index =
@@ -371,7 +371,7 @@ let lambda_implicit_lift n a =
 (* This removes global parameters of the inductive types in lc (for
    nested inductive types only ) *)
 let abstract_mind_lc env ntyps npars lc =
-  if npars = 0 then
+  if Int.equal npars 0 then
     lc
   else
     let make_abs =
@@ -411,7 +411,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
 	  ienv_decompose_prod ienv' (n-1) b
       | _ -> assert false
 
-let array_min nmr a = if nmr = 0 then 0 else
+let array_min nmr a = if Int.equal nmr 0 then 0 else
   Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a
 
 (* The recursive function that checks positivity and builds the list
@@ -620,7 +620,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
     let nconst, nblock = ref 0, ref 0 in
     let transf num =
       let arity = List.length (dest_subterms recarg).(num) in
-	if arity = 0 then
+	if Int.equal arity 0 then
 	  let p  = (!nconst, 0) in
 	    incr nconst; p
 	else
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 81e6c8f17..c53a0bcd9 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -765,7 +765,7 @@ let check_one_fix renv recpos def =
         | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
 
   and check_nested_fix_body renv decr recArgsDecrArg body =
-    if decr = 0 then
+    if Int.equal decr 0 then
       check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
     else
       match kind_of_term body with
@@ -783,7 +783,7 @@ let judgment_of_fixpoint (_, types, bodies) =
 
 let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   let nbfix = Array.length bodies in
-  if nbfix = 0
+  if Int.equal nbfix 0
     or Array.length nvect <> nbfix
     or Array.length types <> nbfix
     or Array.length names <> nbfix
diff --git a/kernel/names.ml b/kernel/names.ml
index 96055ca16..250b4a6b5 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -88,7 +88,7 @@ let rec dir_path_ord (p1 : dir_path) (p2 : dir_path) =
   | _, [] -> 1
   | id1 :: p1, id2 :: p2 ->
     let c = id_ord id1 id2 in
-    if c <> 0 then c else dir_path_ord p1 p2
+    if Int.equal c 0 then dir_path_ord p1 p2 else c
   end
 
 let make_dirpath x = x
@@ -116,11 +116,11 @@ let uniq_ident_ord (x : uniq_ident) (y : uniq_ident) =
   if x == y then 0
   else match (x, y) with
   | (nl, idl, dpl), (nr, idr, dpr) ->
-    let ans = nl - nr in
-    if ans <> 0 then ans
+    let ans = Int.compare nl nr in
+    if not (Int.equal ans 0) then ans
     else
       let ans = id_ord idl idr in
-      if ans <> 0 then ans
+      if not (Int.equal ans 0) then ans
       else
         dir_path_ord dpl dpr
 
@@ -180,7 +180,7 @@ let rec mp_ord mp1 mp2 =
     uniq_ident_ord id1 id2
   | MPdot (mp1, l1), MPdot (mp2, l2) ->
       let c = String.compare l1 l2 in
-        if c <> 0 then c
+        if not (Int.equal c 0) then c
         else mp_ord mp1 mp2
   | MPfile _, _ -> -1
   | MPbound _, MPfile _ -> 1
@@ -226,10 +226,10 @@ let kn_ord (kn1 : kernel_name) (kn2 : kernel_name) =
     let mp1, dir1, l1 = kn1 in
     let mp2, dir2, l2 = kn2 in
     let c = String.compare l1 l2 in
-      if c <> 0 then c
+      if not (Int.equal c 0) then c
       else
         let c = dir_path_ord dir1 dir2 in
-        if c <> 0 then c
+        if not (Int.equal c 0) then c
         else MPord.compare mp1 mp2
 
 module KNord = struct
@@ -259,7 +259,7 @@ let canonical_con con = snd con
 let user_con con = fst con
 let repr_con con = fst con
 
-let eq_constant (_,kn1) (_,kn2) = kn1=kn2
+let eq_constant (_, kn1) (_, kn2) = Int.equal (kn_ord kn1 kn2) 0
 
 let con_label con = label (fst con)
 let con_modpath con = modpath (fst con)
@@ -271,8 +271,9 @@ let debug_string_of_con con =
 let debug_pr_con con = str (debug_string_of_con con)
 
 let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl =
-  if lbl = l1 && lbl = l2 then con
-  else ((mp1,dp1,lbl),(mp2,dp2,lbl))
+  if Int.equal (String.compare lbl l1) 0 && Int.equal (String.compare lbl l2) 0
+    then con
+    else ((mp1, dp1, lbl), (mp2, dp2, lbl))
 
 (** For the environment we distinguish constants by their user part*)
 module User_ord = struct
@@ -319,7 +320,7 @@ let user_mind mind = fst mind
 let repr_mind mind = fst mind
 let mind_label mind = label (fst mind)
 
-let eq_mind (_, kn1) (_, kn2) = kn_ord kn1 kn2 = 0
+let eq_mind (_, kn1) (_, kn2) = Int.equal (kn_ord kn1 kn2) 0
 
 let string_of_mind mind = string_of_kn (fst mind)
 let pr_mind mind = str (string_of_mind mind)
@@ -331,10 +332,10 @@ let ith_mutual_inductive (kn, _) i = (kn, i)
 let ith_constructor_of_inductive ind i = (ind, i)
 let inductive_of_constructor (ind, i) = ind
 let index_of_constructor (ind, i) = i
-let eq_ind (kn1, i1) (kn2, i2) =
-  i1 - i2 = 0 && eq_mind kn1 kn2
-let eq_constructor (kn1, i1) (kn2, i2) =
-  i1 - i2 = 0 && eq_ind kn1 kn2
+
+let eq_ind (kn1, i1) (kn2, i2) = Int.equal i1 i2 && eq_mind kn1 kn2
+
+let eq_constructor (kn1, i1) (kn2, i2) = Int.equal i1 i2 && eq_ind kn1 kn2
 
 module Mindmap = Map.Make(Canonical_ord)
 module Mindset = Set.Make(Canonical_ord)
@@ -343,13 +344,15 @@ module Mindmap_env = Map.Make(User_ord)
 module InductiveOrdered = struct
   type t = inductive
   let compare (spx,ix) (spy,iy) =
-    let c = ix - iy in if c = 0 then Canonical_ord.compare spx spy else c
+    let c = Int.compare ix iy in
+    if Int.equal c 0 then Canonical_ord.compare spx spy else c
 end
 
 module InductiveOrdered_env = struct
   type t = inductive
   let compare (spx,ix) (spy,iy) =
-    let c = ix - iy in if c = 0 then User_ord.compare spx spy else c
+    let c = Int.compare ix iy in
+    if Int.equal c 0 then User_ord.compare spx spy else c
 end
 
 module Indmap = Map.Make(InductiveOrdered)
@@ -358,13 +361,15 @@ module Indmap_env = Map.Make(InductiveOrdered_env)
 module ConstructorOrdered = struct
   type t = constructor
   let compare (indx,ix) (indy,iy) =
-    let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c
+    let c = Int.compare ix iy in
+    if Int.equal c 0 then InductiveOrdered.compare indx indy else c
 end
 
 module ConstructorOrdered_env = struct
   type t = constructor
   let compare (indx,ix) (indy,iy) =
-    let c = ix - iy in if c = 0 then InductiveOrdered_env.compare indx indy else c
+    let c = Int.compare ix iy in
+    if Int.equal c 0 then InductiveOrdered_env.compare indx indy else c
 end
 
 module Constrmap = Map.Make(ConstructorOrdered)
@@ -418,7 +423,7 @@ module Huniqid = Hashcons.Make(
     let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
     let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
       (x == y) ||
-      (n1 - n2 = 0 && s1 == s2 && dir1 == dir2)
+      (Int.equal n1 n2 && s1 == s2 && dir1 == dir2)
     let hash = Hashtbl.hash
   end)
 
@@ -471,7 +476,7 @@ module Hind = Hashcons.Make(
     type t = inductive
     type u = mutual_inductive -> mutual_inductive
     let hashcons hmind (mind, i) = (hmind mind, i)
-    let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && i1 = i2
+    let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
     let hash = Hashtbl.hash
   end)
 
@@ -480,7 +485,7 @@ module Hconstruct = Hashcons.Make(
     type t = constructor
     type u = inductive -> inductive
     let hashcons hind (ind, j) = (hind ind, j)
-    let equal (ind1,j1) (ind2,j2) = ind1 == ind2 && (j1 - j2 = 0)
+    let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
     let hash = Hashtbl.hash
   end)
 
@@ -522,15 +527,14 @@ let eq_id_key ik1 ik2 =
   if ik1 == ik2 then true
   else match ik1,ik2 with
   | ConstKey (u1, kn1), ConstKey (u2, kn2) ->
-    let ans = (kn_ord u1 u2 = 0) in
-    if ans then kn_ord kn1 kn2 = 0
+    let ans = Int.equal (kn_ord u1 u2) 0 in
+    if ans then Int.equal (kn_ord kn1 kn2) 0
     else ans
   | VarKey id1, VarKey id2 ->
-    id_ord id1 id2 = 0
-  | RelKey k1, RelKey k2 ->
-    k1 - k2 = 0
+    Int.equal (id_ord id1 id2) 0
+  | RelKey k1, RelKey k2 -> Int.equal k1 k2
   | _ -> false
 
-let eq_con_chk (kn1,_) (kn2,_) = kn1=kn2
-let eq_mind_chk (kn1,_) (kn2,_) = kn1=kn2
-let eq_ind_chk (kn1,i1) (kn2,i2) = i1=i2&&eq_mind_chk kn1 kn2
+let eq_con_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0
+let eq_mind_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0
+let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 76dcd1d3a..1d974eada 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -129,7 +129,7 @@ let beta_appvect c v =
 
 let betazeta_appvect n c v =
   let rec stacklam n env t stack =
-    if n = 0 then applist (substl env t, stack) else
+    if Int.equal n 0 then applist (substl env t, stack) else
     match kind_of_term t, stack with
         Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
       | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
@@ -205,7 +205,7 @@ let rec no_arg_available = function
   | [] -> true
   | Zupdate _ :: stk -> no_arg_available stk
   | Zshift _ :: stk -> no_arg_available stk
-  | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk
+  | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk
   | Zcase _ :: _ -> true
   | Zfix _ :: _ -> true
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index b8626e227..8b34950da 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -191,10 +191,10 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
       | Cast(t,_,_) -> names_prod_letin t
       | _ -> []
     in
-    assert (Array.length mib1.mind_packets = 1);
-    assert (Array.length mib2.mind_packets = 1);
-    assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1);
-    assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1);
+    assert (Int.equal (Array.length mib1.mind_packets) 1);
+    assert (Int.equal (Array.length mib2.mind_packets) 1);
+    assert (Int.equal (Array.length mib1.mind_packets.(0).mind_user_lc) 1);
+    assert (Int.equal (Array.length mib2.mind_packets.(0).mind_user_lc) 1);
     check (fun mib ->
       let nparamdecls = List.length mib.mind_params_ctxt in
       let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in
diff --git a/kernel/term.ml b/kernel/term.ml
index 0937fc16b..a99262adf 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -154,7 +154,7 @@ let mkLetIn (x,c1,t,c2) = LetIn (x,c1,t,c2)
 (* We ensure applicative terms have at least one argument and the
    function is not itself an applicative term *)
 let mkApp (f, a) =
-  if Array.length a = 0 then f else
+  if Int.equal (Array.length a) 0 then f else
     match f with
       | App (g, cl) -> App (g, Array.append cl a)
       | _ -> App (f, a)
@@ -623,10 +623,13 @@ let constr_ord_int f t1 t2 =
 	((-) =? (Array.compare f)) e1 e2 l1 l2
     | Const c1, Const c2 -> kn_ord (canonical_con c1) (canonical_con c2)
     | Ind (spx, ix), Ind (spy, iy) ->
-	let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c
+        let c = Int.compare ix iy in
+        if Int.equal c 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c
     | Construct ((spx, ix), jx), Construct ((spy, iy), jy) ->
-	let c = jx - jy in if c = 0 then
-	  (let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c)
+        let c = Int.compare jx jy in
+        if Int.equal c 0 then
+	  (let c = Int.compare ix iy in
+          if Int.equal c 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c)
 	else c
     | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
 	((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2
@@ -665,7 +668,7 @@ 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_ord i1 i2 = 0 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
+  Int.equal (id_ord i1 i2) 0 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
 
 let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) =
   n1 = n2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
@@ -805,7 +808,7 @@ let make_substituend c = { sinfo=Unknown; sit=c }
 
 let substn_many lamv n c =
   let lv = Array.length lamv in
-  if lv = 0 then c
+  if Int.equal lv 0 then c
   else
     let rec substrec depth c = match kind_of_term c with
       | Rel k     ->
@@ -947,7 +950,7 @@ let appvectc f l = mkApp (f,l)
 (* to_lambda n (x1:T1)...(xn:Tn)T =
  * [x1:T1]...[xn:Tn]T *)
 let rec to_lambda n prod =
-  if n = 0 then
+  if Int.equal n 0 then
     prod
   else
     match kind_of_term prod with
@@ -956,7 +959,7 @@ let rec to_lambda n prod =
       | _   -> errorlabstrm "to_lambda" (mt ())
 
 let rec to_prod n lam =
-  if n=0 then
+  if Int.equal n 0 then
     lam
   else
     match kind_of_term lam with
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 635991494..bdd668cbd 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) ->
-      i1 = i2 && (Names.dir_path_ord dp1 dp2 = 0)
+      Int.equal i1 i2 && Int.equal (Names.dir_path_ord dp1 dp2) 0
     | _ -> false
 
   let to_string = function
@@ -725,7 +725,7 @@ let sort_universes orig =
     let accu, continue = UniverseLMap.fold (fun u x (accu, continue) ->
       let continue = continue || x < 0 in
       let accu =
-        if x = 0 && u != type0 then UniverseLMap.add u i accu
+        if Int.equal x 0 && u != type0 then UniverseLMap.add u i accu
         else accu
       in accu, continue) distances (accu, false)
     in
diff --git a/kernel/vm.ml b/kernel/vm.ml
index d4a86cb49..b6a39b042 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -169,7 +169,7 @@ type whd =
 
 let rec whd_accu a stk =
   let stk =
-    if Obj.size a = 2 then stk
+    if Int.equal (Obj.size a) 2 then stk
     else Zapp (Obj.obj a) :: stk in
   let at = Obj.field a 1 in
   match Obj.tag at with
@@ -211,7 +211,7 @@ let whd_val : values -> whd =
       let tag = Obj.tag o in
       if tag = accu_tag then
 	(
-	if Obj.size o = 1 then Obj.obj o (* sort *)
+	if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *)
 	else
 	  if is_accumulate (fun_code o) then whd_accu o []
 	  else (Vprod(Obj.obj o)))
@@ -255,7 +255,7 @@ let arg args i =
 
 let apply_arguments vf vargs =
   let n = nargs vargs in
-  if n = 0 then vf
+  if Int.equal n 0 then vf
   else
    begin
      push_ra stop;
@@ -265,7 +265,7 @@ let apply_arguments vf vargs =
 
 let apply_vstack vf vstk =
   let n = Array.length vstk in
-  if n = 0 then vf
+  if Int.equal n 0 then vf
   else
     begin
       push_ra stop;
@@ -502,7 +502,7 @@ let type_of_switch sw =
   interprete sw.sw_type_code crazy_val sw.sw_env 0
 
 let branch_arg k (tag,arity) =
-  if arity = 0 then  ((Obj.magic tag):values)
+  if Int.equal arity 0 then  ((Obj.magic tag):values)
   else
     let b = Obj.new_block tag arity in
     for i = 0 to arity - 1 do