From b0b1710ba631f3a3a3faad6e955ef703c67cb967 Mon Sep 17 00:00:00 2001
From: ppedrot
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/inductive.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 81e6c8f170..c53a0bcd90 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -765,7 +765,7 @@ let check_one_fix renv recpos def =
         | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
 
   and check_nested_fix_body renv decr recArgsDecrArg body =
-    if decr = 0 then
+    if Int.equal decr 0 then
       check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
     else
       match kind_of_term body with
@@ -783,7 +783,7 @@ let judgment_of_fixpoint (_, types, bodies) =
 
 let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   let nbfix = Array.length bodies in
-  if nbfix = 0
+  if Int.equal nbfix 0
     or Array.length nvect <> nbfix
     or Array.length types <> nbfix
     or Array.length names <> nbfix
-- 
cgit v1.2.3