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, 3 insertions, 3 deletions

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