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/lib/pp.ml b/lib/pp.ml
index 5a38b08c39..71c72baa90 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -236,7 +236,7 @@ let rec pr_com ft s =
   Format.pp_print_as ft (utf8_length s1) s1;
   match os with
       Some s2 ->
-        if String.length s2 = 0 then (com_eol := true)
+        if Int.equal (String.length s2) 0 then (com_eol := true)
         else
           (Format.pp_force_newline ft (); pr_com ft s2)
     | None -> ()
@@ -441,14 +441,14 @@ let pr_vertical_list pr = function
 
 let prvecti_with_sep sep elem v =
   let rec pr i =
-    if i = 0 then
+    if Int.equal i 0 then
       elem 0 v.(0)
     else
       let r = pr (i-1) and s = sep () and e = elem i v.(i) in
       r ++ s ++ e
   in
   let n = Array.length v in
-  if n = 0 then mt () else pr (n - 1)
+  if Int.equal n 0 then mt () else pr (n - 1)
 
 (* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *)