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

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 9e695e3d3d..deba56f733 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)