Monomorphization (pretyping)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15994 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 2 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 099a2ab76..cb71e1aa6 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -85,7 +85,7 @@ let rec shift_value n = function
   | CONSTR (c,args) ->
       CONSTR (c, Array.map (shift_value n) args)
 let shift_value n v =
-  if n = 0 then v else shift_value n v
+  if Int.equal n 0 then v else shift_value n v
 
 (* Contracts a fixpoint: given a fixpoint and a bindings,
  * returns the corresponding fixpoint body, and the bindings in which
@@ -110,7 +110,7 @@ let make_constr_ref n = function
 
 (* Adds an application list. Collapse APPs! *)
 let stack_app appl stack =
-  if Array.length appl = 0 then stack else
+  if Int.equal (Array.length appl) 0 then stack else
     match stack with
     | APP(args,stk) -> APP(Array.append appl args,stk)
     | _             -> APP(appl, stack)