From b0b1710ba631f3a3a3faad6e955ef703c67cb967 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 8 Nov 2012 17:11:59 +0000
Subject: 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
---
 kernel/vm.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel/vm.ml')

diff --git a/kernel/vm.ml b/kernel/vm.ml
index d4a86cb49..b6a39b042 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -169,7 +169,7 @@ type whd =
 
 let rec whd_accu a stk =
   let stk =
-    if Obj.size a = 2 then stk
+    if Int.equal (Obj.size a) 2 then stk
     else Zapp (Obj.obj a) :: stk in
   let at = Obj.field a 1 in
   match Obj.tag at with
@@ -211,7 +211,7 @@ let whd_val : values -> whd =
       let tag = Obj.tag o in
       if tag = accu_tag then
 	(
-	if Obj.size o = 1 then Obj.obj o (* sort *)
+	if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *)
 	else
 	  if is_accumulate (fun_code o) then whd_accu o []
 	  else (Vprod(Obj.obj o)))
@@ -255,7 +255,7 @@ let arg args i =
 
 let apply_arguments vf vargs =
   let n = nargs vargs in
-  if n = 0 then vf
+  if Int.equal n 0 then vf
   else
    begin
      push_ra stop;
@@ -265,7 +265,7 @@ let apply_arguments vf vargs =
 
 let apply_vstack vf vstk =
   let n = Array.length vstk in
-  if n = 0 then vf
+  if Int.equal n 0 then vf
   else
     begin
       push_ra stop;
@@ -502,7 +502,7 @@ let type_of_switch sw =
   interprete sw.sw_type_code crazy_val sw.sw_env 0
 
 let branch_arg k (tag,arity) =
-  if arity = 0 then  ((Obj.magic tag):values)
+  if Int.equal arity 0 then  ((Obj.magic tag):values)
   else
     let b = Obj.new_block tag arity in
     for i = 0 to arity - 1 do
-- 
cgit v1.2.3