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

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