diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 81e6c8f17..c53a0bcd9 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 |