diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cbytegen.ml | 24 | ||||
| -rw-r--r-- | kernel/cemitcodes.ml | 6 | ||||
| -rw-r--r-- | kernel/closure.ml | 8 | ||||
| -rw-r--r-- | kernel/environ.ml | 2 | ||||
| -rw-r--r-- | kernel/esubst.ml | 12 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 8 | ||||
| -rw-r--r-- | kernel/inductive.ml | 4 | ||||
| -rw-r--r-- | kernel/names.ml | 64 | ||||
| -rw-r--r-- | kernel/reduction.ml | 4 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 8 | ||||
| -rw-r--r-- | kernel/term.ml | 19 | ||||
| -rw-r--r-- | kernel/univ.ml | 4 | ||||
| -rw-r--r-- | kernel/vm.ml | 10 |
13 files changed, 90 insertions, 83 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 9e695e3d3..deba56f73 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) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 680a5f9f2..90b4f0ae0 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -165,7 +165,7 @@ let emit_instr = function then out(opENVACC1 + n - 1) else (out opENVACC; out_int n) | Koffsetclosure ofs -> - if ofs = -2 || ofs = 0 || ofs = 2 + if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2 then out (opOFFSETCLOSURE0 + ofs / 2) else (out opOFFSETCLOSURE; out_int ofs) | Kpush -> @@ -214,7 +214,7 @@ let emit_instr = function | Kconst c -> out opGETGLOBAL; slot_for_const c | Kmakeblock(n, t) -> - if n = 0 then raise (Invalid_argument "emit_instr : block size = 0") + if Int.equal n 0 then raise (Invalid_argument "emit_instr : block size = 0") else if n < 4 then (out(opMAKEBLOCK1 + n - 1); out_int t) else (out opMAKEBLOCK; out_int n; out_int t) | Kmakeprod -> @@ -279,7 +279,7 @@ let rec emit = function else (out opPUSHENVACC; out_int n); emit c | Kpush :: Koffsetclosure ofs :: c -> - if ofs = -2 || ofs = 0 || ofs = 2 + if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2 then out(opPUSHOFFSETCLOSURE0 + ofs / 2) else (out opPUSHOFFSETCLOSURE; out_int ofs); emit c diff --git a/kernel/closure.ml b/kernel/closure.ml index 51e264106..681fb8533 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -354,7 +354,7 @@ and stack = stack_member list let empty_stack = [] let append_stack v s = - if Array.length v = 0 then s else + if Int.equal (Array.length v) 0 then s else match s with | Zapp l :: s -> Zapp (Array.append v l) :: s | _ -> Zapp v :: s @@ -398,7 +398,7 @@ let rec stack_assign s p c = match s with Zapp nargs :: s) | _ -> s let rec stack_tail p s = - if p = 0 then s else + if Int.equal p 0 then s else match s with | Zapp args :: s -> let q = Array.length args in @@ -719,7 +719,7 @@ let get_nth_arg head n stk = let bef = Array.sub args 0 n in let aft = Array.sub args (n+1) (q-n-1) in let stk' = - List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in + List.rev (if Int.equal n 0 then rstk else (Zapp bef :: rstk)) in (Some (stk', args.(n)), append_stack aft s') | Zupdate(m)::s -> strip_rec rstk (update m (h.norm,h.term)) n s @@ -764,7 +764,7 @@ let rec reloc_rargs_rec depth stk = | _ -> stk let reloc_rargs depth stk = - if depth = 0 then stk else reloc_rargs_rec depth stk + if Int.equal depth 0 then stk else reloc_rargs_rec depth stk let rec drop_parameters depth n argstk = match argstk with diff --git a/kernel/environ.ml b/kernel/environ.ml index 37a896c77..301c3b152 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -423,7 +423,7 @@ let register = let nth_digit_plus_one i n = (* calculates the nth (starting with 0) digit of i and adds 1 to it (nth_digit_plus_one 1 3 = 2) *) - if (land) i ((lsl) 1 n) = 0 then + if Int.equal (i land (1 lsl n)) 0 then 1 else 2 diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 0bd7c515c..30c2387ea 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -29,14 +29,14 @@ let el_id = ELID let rec el_shft_rec n = function | ELSHFT(el,k) -> el_shft_rec (k+n) el | el -> ELSHFT(el,n) -let el_shft n el = if n = 0 then el else el_shft_rec n el +let el_shft n el = if Int.equal n 0 then el else el_shft_rec n el (* cross n binders *) let rec el_liftn_rec n = function | ELID -> ELID | ELLFT(k,el) -> el_liftn_rec (n+k) el | el -> ELLFT(n, el) -let el_liftn n el = if n = 0 then el else el_liftn_rec n el +let el_liftn n el = if Int.equal n 0 then el else el_liftn_rec n el let el_lift el = el_liftn_rec 1 el @@ -73,7 +73,7 @@ type 'a subs = let subs_id i = ESID i -let subs_cons(x,s) = if Array.length x = 0 then s else CONS(x,s) +let subs_cons(x,s) = if Int.equal (Array.length x) 0 then s else CONS(x,s) let subs_liftn n = function | ESID p -> ESID (p+n) (* bounded identity lifted extends by p *) @@ -81,13 +81,13 @@ let subs_liftn n = function | lenv -> LIFT (n,lenv) let subs_lift a = subs_liftn 1 a -let subs_liftn n a = if n = 0 then a else subs_liftn n a +let subs_liftn n a = if Int.equal n 0 then a else subs_liftn n a let subs_shft = function | (0, s) -> s | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1) | (n, s) -> SHIFT (n,s) -let subs_shft (n,a) = if n = 0 then a else subs_shft(n,a) +let subs_shft (n,a) = if Int.equal n 0 then a else subs_shft(n,a) let subs_shift_cons = function (0, s, t) -> CONS(t,s) @@ -99,7 +99,7 @@ let rec is_subs_id = function ESID _ -> true | LIFT(_,s) -> is_subs_id s | SHIFT(0,s) -> is_subs_id s - | CONS(x,s) -> Array.length x = 0 && is_subs_id s + | CONS(x,s) -> Int.equal (Array.length x) 0 && is_subs_id s | _ -> false (* Expands de Bruijn k in the explicit substitution subs diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 1c12c9e24..6b993604d 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -349,7 +349,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = recursive parameters *) let compute_rec_par (env,n,_,_) hyps nmr largs = -if nmr = 0 then 0 else +if Int.equal nmr 0 then 0 else (* start from 0, hyps will be in reverse order *) let (lpar,_) = List.chop nmr largs in let rec find k index = @@ -371,7 +371,7 @@ let lambda_implicit_lift n a = (* This removes global parameters of the inductive types in lc (for nested inductive types only ) *) let abstract_mind_lc env ntyps npars lc = - if npars = 0 then + if Int.equal npars 0 then lc else let make_abs = @@ -411,7 +411,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = ienv_decompose_prod ienv' (n-1) b | _ -> assert false -let array_min nmr a = if nmr = 0 then 0 else +let array_min nmr a = if Int.equal nmr 0 then 0 else Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a (* The recursive function that checks positivity and builds the list @@ -620,7 +620,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = let nconst, nblock = ref 0, ref 0 in let transf num = let arity = List.length (dest_subterms recarg).(num) in - if arity = 0 then + if Int.equal arity 0 then let p = (!nconst, 0) in incr nconst; p else 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 diff --git a/kernel/names.ml b/kernel/names.ml index 96055ca16..250b4a6b5 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -88,7 +88,7 @@ let rec dir_path_ord (p1 : dir_path) (p2 : dir_path) = | _, [] -> 1 | id1 :: p1, id2 :: p2 -> let c = id_ord id1 id2 in - if c <> 0 then c else dir_path_ord p1 p2 + if Int.equal c 0 then dir_path_ord p1 p2 else c end let make_dirpath x = x @@ -116,11 +116,11 @@ let uniq_ident_ord (x : uniq_ident) (y : uniq_ident) = if x == y then 0 else match (x, y) with | (nl, idl, dpl), (nr, idr, dpr) -> - let ans = nl - nr in - if ans <> 0 then ans + let ans = Int.compare nl nr in + if not (Int.equal ans 0) then ans else let ans = id_ord idl idr in - if ans <> 0 then ans + if not (Int.equal ans 0) then ans else dir_path_ord dpl dpr @@ -180,7 +180,7 @@ let rec mp_ord mp1 mp2 = uniq_ident_ord id1 id2 | MPdot (mp1, l1), MPdot (mp2, l2) -> let c = String.compare l1 l2 in - if c <> 0 then c + if not (Int.equal c 0) then c else mp_ord mp1 mp2 | MPfile _, _ -> -1 | MPbound _, MPfile _ -> 1 @@ -226,10 +226,10 @@ let kn_ord (kn1 : kernel_name) (kn2 : kernel_name) = let mp1, dir1, l1 = kn1 in let mp2, dir2, l2 = kn2 in let c = String.compare l1 l2 in - if c <> 0 then c + if not (Int.equal c 0) then c else let c = dir_path_ord dir1 dir2 in - if c <> 0 then c + if not (Int.equal c 0) then c else MPord.compare mp1 mp2 module KNord = struct @@ -259,7 +259,7 @@ let canonical_con con = snd con let user_con con = fst con let repr_con con = fst con -let eq_constant (_,kn1) (_,kn2) = kn1=kn2 +let eq_constant (_, kn1) (_, kn2) = Int.equal (kn_ord kn1 kn2) 0 let con_label con = label (fst con) let con_modpath con = modpath (fst con) @@ -271,8 +271,9 @@ let debug_string_of_con con = let debug_pr_con con = str (debug_string_of_con con) let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl = - if lbl = l1 && lbl = l2 then con - else ((mp1,dp1,lbl),(mp2,dp2,lbl)) + if Int.equal (String.compare lbl l1) 0 && Int.equal (String.compare lbl l2) 0 + then con + else ((mp1, dp1, lbl), (mp2, dp2, lbl)) (** For the environment we distinguish constants by their user part*) module User_ord = struct @@ -319,7 +320,7 @@ let user_mind mind = fst mind let repr_mind mind = fst mind let mind_label mind = label (fst mind) -let eq_mind (_, kn1) (_, kn2) = kn_ord kn1 kn2 = 0 +let eq_mind (_, kn1) (_, kn2) = Int.equal (kn_ord kn1 kn2) 0 let string_of_mind mind = string_of_kn (fst mind) let pr_mind mind = str (string_of_mind mind) @@ -331,10 +332,10 @@ let ith_mutual_inductive (kn, _) i = (kn, i) let ith_constructor_of_inductive ind i = (ind, i) let inductive_of_constructor (ind, i) = ind let index_of_constructor (ind, i) = i -let eq_ind (kn1, i1) (kn2, i2) = - i1 - i2 = 0 && eq_mind kn1 kn2 -let eq_constructor (kn1, i1) (kn2, i2) = - i1 - i2 = 0 && eq_ind kn1 kn2 + +let eq_ind (kn1, i1) (kn2, i2) = Int.equal i1 i2 && eq_mind kn1 kn2 + +let eq_constructor (kn1, i1) (kn2, i2) = Int.equal i1 i2 && eq_ind kn1 kn2 module Mindmap = Map.Make(Canonical_ord) module Mindset = Set.Make(Canonical_ord) @@ -343,13 +344,15 @@ module Mindmap_env = Map.Make(User_ord) module InductiveOrdered = struct type t = inductive let compare (spx,ix) (spy,iy) = - let c = ix - iy in if c = 0 then Canonical_ord.compare spx spy else c + let c = Int.compare ix iy in + if Int.equal c 0 then Canonical_ord.compare spx spy else c end module InductiveOrdered_env = struct type t = inductive let compare (spx,ix) (spy,iy) = - let c = ix - iy in if c = 0 then User_ord.compare spx spy else c + let c = Int.compare ix iy in + if Int.equal c 0 then User_ord.compare spx spy else c end module Indmap = Map.Make(InductiveOrdered) @@ -358,13 +361,15 @@ module Indmap_env = Map.Make(InductiveOrdered_env) module ConstructorOrdered = struct type t = constructor let compare (indx,ix) (indy,iy) = - let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c + let c = Int.compare ix iy in + if Int.equal c 0 then InductiveOrdered.compare indx indy else c end module ConstructorOrdered_env = struct type t = constructor let compare (indx,ix) (indy,iy) = - let c = ix - iy in if c = 0 then InductiveOrdered_env.compare indx indy else c + let c = Int.compare ix iy in + if Int.equal c 0 then InductiveOrdered_env.compare indx indy else c end module Constrmap = Map.Make(ConstructorOrdered) @@ -418,7 +423,7 @@ module Huniqid = Hashcons.Make( let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir) let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = (x == y) || - (n1 - n2 = 0 && s1 == s2 && dir1 == dir2) + (Int.equal n1 n2 && s1 == s2 && dir1 == dir2) let hash = Hashtbl.hash end) @@ -471,7 +476,7 @@ module Hind = Hashcons.Make( type t = inductive type u = mutual_inductive -> mutual_inductive let hashcons hmind (mind, i) = (hmind mind, i) - let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && i1 = i2 + let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 let hash = Hashtbl.hash end) @@ -480,7 +485,7 @@ module Hconstruct = Hashcons.Make( type t = constructor type u = inductive -> inductive let hashcons hind (ind, j) = (hind ind, j) - let equal (ind1,j1) (ind2,j2) = ind1 == ind2 && (j1 - j2 = 0) + let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 let hash = Hashtbl.hash end) @@ -522,15 +527,14 @@ let eq_id_key ik1 ik2 = if ik1 == ik2 then true else match ik1,ik2 with | ConstKey (u1, kn1), ConstKey (u2, kn2) -> - let ans = (kn_ord u1 u2 = 0) in - if ans then kn_ord kn1 kn2 = 0 + let ans = Int.equal (kn_ord u1 u2) 0 in + if ans then Int.equal (kn_ord kn1 kn2) 0 else ans | VarKey id1, VarKey id2 -> - id_ord id1 id2 = 0 - | RelKey k1, RelKey k2 -> - k1 - k2 = 0 + Int.equal (id_ord id1 id2) 0 + | RelKey k1, RelKey k2 -> Int.equal k1 k2 | _ -> false -let eq_con_chk (kn1,_) (kn2,_) = kn1=kn2 -let eq_mind_chk (kn1,_) (kn2,_) = kn1=kn2 -let eq_ind_chk (kn1,i1) (kn2,i2) = i1=i2&&eq_mind_chk kn1 kn2 +let eq_con_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0 +let eq_mind_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0 +let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2 diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 76dcd1d3a..1d974eada 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -129,7 +129,7 @@ let beta_appvect c v = let betazeta_appvect n c v = let rec stacklam n env t stack = - if n = 0 then applist (substl env t, stack) else + if Int.equal n 0 then applist (substl env t, stack) else match kind_of_term t, stack with Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack @@ -205,7 +205,7 @@ let rec no_arg_available = function | [] -> true | Zupdate _ :: stk -> no_arg_available stk | Zshift _ :: stk -> no_arg_available stk - | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk + | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk | Zcase _ :: _ -> true | Zfix _ :: _ -> true diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index b8626e227..8b34950da 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -191,10 +191,10 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 | Cast(t,_,_) -> names_prod_letin t | _ -> [] in - assert (Array.length mib1.mind_packets = 1); - assert (Array.length mib2.mind_packets = 1); - assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1); - assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1); + assert (Int.equal (Array.length mib1.mind_packets) 1); + assert (Int.equal (Array.length mib2.mind_packets) 1); + assert (Int.equal (Array.length mib1.mind_packets.(0).mind_user_lc) 1); + assert (Int.equal (Array.length mib2.mind_packets.(0).mind_user_lc) 1); check (fun mib -> let nparamdecls = List.length mib.mind_params_ctxt in let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in diff --git a/kernel/term.ml b/kernel/term.ml index 0937fc16b..a99262adf 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -154,7 +154,7 @@ let mkLetIn (x,c1,t,c2) = LetIn (x,c1,t,c2) (* We ensure applicative terms have at least one argument and the function is not itself an applicative term *) let mkApp (f, a) = - if Array.length a = 0 then f else + if Int.equal (Array.length a) 0 then f else match f with | App (g, cl) -> App (g, Array.append cl a) | _ -> App (f, a) @@ -623,10 +623,13 @@ let constr_ord_int f t1 t2 = ((-) =? (Array.compare f)) e1 e2 l1 l2 | Const c1, Const c2 -> kn_ord (canonical_con c1) (canonical_con c2) | Ind (spx, ix), Ind (spy, iy) -> - let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c + let c = Int.compare ix iy in + if Int.equal c 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c | Construct ((spx, ix), jx), Construct ((spy, iy), jy) -> - let c = jx - jy in if c = 0 then - (let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c) + let c = Int.compare jx jy in + if Int.equal c 0 then + (let c = Int.compare ix iy in + if Int.equal c 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c) else c | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2 @@ -665,7 +668,7 @@ let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = - id_ord i1 i2 = 0 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2 + Int.equal (id_ord i1 i2) 0 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2 let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) = n1 = n2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2 @@ -805,7 +808,7 @@ let make_substituend c = { sinfo=Unknown; sit=c } let substn_many lamv n c = let lv = Array.length lamv in - if lv = 0 then c + if Int.equal lv 0 then c else let rec substrec depth c = match kind_of_term c with | Rel k -> @@ -947,7 +950,7 @@ let appvectc f l = mkApp (f,l) (* to_lambda n (x1:T1)...(xn:Tn)T = * [x1:T1]...[xn:Tn]T *) let rec to_lambda n prod = - if n = 0 then + if Int.equal n 0 then prod else match kind_of_term prod with @@ -956,7 +959,7 @@ let rec to_lambda n prod = | _ -> errorlabstrm "to_lambda" (mt ()) let rec to_prod n lam = - if n=0 then + if Int.equal n 0 then lam else match kind_of_term lam with diff --git a/kernel/univ.ml b/kernel/univ.ml index 635991494..bdd668cbd 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -58,7 +58,7 @@ module UniverseLevel = struct let equal u v = match u,v with | Set, Set -> true | Level (i1, dp1), Level (i2, dp2) -> - i1 = i2 && (Names.dir_path_ord dp1 dp2 = 0) + Int.equal i1 i2 && Int.equal (Names.dir_path_ord dp1 dp2) 0 | _ -> false let to_string = function @@ -725,7 +725,7 @@ let sort_universes orig = let accu, continue = UniverseLMap.fold (fun u x (accu, continue) -> let continue = continue || x < 0 in let accu = - if x = 0 && u != type0 then UniverseLMap.add u i accu + if Int.equal x 0 && u != type0 then UniverseLMap.add u i accu else accu in accu, continue) distances (accu, false) in 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 |