1 files changed, 6 insertions, 6 deletions
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