diff options
59 files changed, 276 insertions, 259 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d5f96e3fd..b651053db 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -274,7 +274,7 @@ let drop_implicits_in_patt cst nb_expl args = |None -> aux t |x -> x in - if nb_expl = 0 then aux impl_data + if Int.equal nb_expl 0 then aux impl_data else let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in impls_fit [] (imps,args) @@ -712,7 +712,7 @@ let rec extern inctx scopes vars r = let projs = struc.Recordops.s_PROJ in let locals = struc.Recordops.s_PROJKIND in let rec cut args n = - if n = 0 then args + if Int.equal n 0 then args else match args with | [] -> raise No_match @@ -907,7 +907,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function subscopes,impls | _ -> [], [] in - (if n = 0 then f else GApp (Loc.ghost,f,args1)), + (if Int.equal n 0 then f else GApp (Loc.ghost,f,args1)), args2, subscopes, impls | GApp (_,(GRef (_,ref) as f),args), None -> let subscopes = find_arguments_scope ref in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c204db0e0..a6b207c1d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -199,7 +199,7 @@ and spaces ntn n = let expand_notation_string ntn n = let pos = List.nth (wildcards ntn 0) n in - let hd = if pos = 0 then "" else String.sub ntn 0 pos in + let hd = if Int.equal pos 0 then "" else String.sub ntn 0 pos in let tl = if pos = String.length ntn then "" else String.sub ntn (pos+1) (String.length ntn - pos -1) in @@ -737,7 +737,7 @@ let find_remaining_scopes pl1 pl2 ref = let impls_st = implicits_of_global ref in let len_pl1 = List.length pl1 in let len_pl2 = List.length pl2 in - let impl_list = if len_pl1 = 0 + let impl_list = if Int.equal len_pl1 0 then select_impargs_size len_pl2 impls_st else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in let allscs = find_arguments_scope ref in @@ -797,7 +797,7 @@ let check_constructor_length env loc cstr len_pl pl0 = (nargs - (Inductiveops.inductive_nparams (fst cstr)))) let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 = - let impl_list = if len_pl1 = 0 + let impl_list = if Int.equal len_pl1 0 then select_impargs_size (List.length pl2) impls_st else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index c5cc1438b..d3c55c1f5 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -754,7 +754,7 @@ let rec match_cases_pattern metas sigma a1 a2 = when r1 = r2 -> let l1 = add_patterns_for_params (fst r1) args1 in let le2 = List.length l2 in - if le2 = 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 + if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 then raise No_match else @@ -777,7 +777,7 @@ let match_ind_pattern metas sigma ind pats a2 = | NApp (NRef (IndRef r2),l2) when ind = r2 -> let le2 = List.length l2 in - if le2 = 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats + if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats then raise No_match else 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 diff --git a/lib/bigint.ml b/lib/bigint.ml index 9012d9322..be207f667 100644 --- a/lib/bigint.ml +++ b/lib/bigint.ml @@ -43,8 +43,8 @@ let size = let format_size = (* How to parametrize a printf format *) - if size = 4 then Printf.sprintf "%04d" - else if size = 9 then Printf.sprintf "%09d" + if Int.equal size 4 then Printf.sprintf "%04d" + else if Int.equal size 9 then Printf.sprintf "%09d" else fun n -> let rec aux j l n = if j=size then l else aux (j+1) (string_of_int (n mod 10) :: l) (n/10) @@ -73,7 +73,7 @@ let neg_one = [|-1|] let canonical n = let ok x = (0 <= x && x < base) in - let rec ok_tail k = (k = 0) || (ok n.(k) && ok_tail (k-1)) in + let rec ok_tail k = (Int.equal k 0) || (ok n.(k) && ok_tail (k-1)) in let ok_init x = (-base <= x && x < base && x <> -1 && x <> 0) in (n = [||]) || (n = [|-1|]) || @@ -83,7 +83,7 @@ let canonical n = let normalize_pos n = let k = ref 0 in - while !k < Array.length n & n.(!k) = 0 do incr k done; + while !k < Array.length n && Int.equal n.(!k) 0 do incr k done; Array.sub n !k (Array.length n - !k) (* [normalize_neg] : avoid (-1) as first bloc. @@ -94,16 +94,16 @@ let normalize_neg n = let k = ref 1 in while !k < Array.length n & n.(!k) = base - 1 do incr k done; let n' = Array.sub n !k (Array.length n - !k) in - if Array.length n' = 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n') + if Int.equal (Array.length n') 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n') (* [normalize] : avoid 0 and (-1) as first bloc. input: an array with first bloc in [-base;base[ and others in [0;base[ output: a canonical array *) let normalize n = - if Array.length n = 0 then n - else if n.(0) = -1 then normalize_neg n - else if n.(0) = 0 then normalize_pos n + if Int.equal (Array.length n) 0 then n + else if Int.equal n.(0) (-1) then normalize_neg n + else if Int.equal n.(0) 0 then normalize_pos n else n (* Opposite (expects and returns canonical arrays) *) @@ -112,8 +112,8 @@ let neg m = if m = zero then zero else let n = Array.copy m in let i = ref (Array.length m - 1) in - while !i > 0 & n.(!i) = 0 do decr i done; - if !i = 0 then begin + while !i > 0 && Int.equal n.(!i) 0 do decr i done; + if Int.equal !i 0 then begin n.(0) <- - n.(0); (* n.(0) cannot be 0 since m is canonical *) if n.(0) = -1 then normalize_neg n @@ -261,7 +261,7 @@ let euclid m d = let q = Array.create (ql+1) 0 in let i = ref 0 in while not (less_than_shift_pos !i m d) do - if m.(!i)=0 then incr i else + if Int.equal m.(!i) 0 then incr i else if can_divide !i m d 0 then begin let v = if Array.length d > 1 && d.(0) <> m.(!i) then @@ -297,14 +297,14 @@ let of_string s = let e = if h<>"" then 1 else 0 in let l = (len - !d) / size in let a = Array.create (l + e) 0 in - if e=1 then a.(0) <- int_of_string h; - for i=1 to l do + if Int.equal e 1 then a.(0) <- int_of_string h; + for i = 1 to l do a.(i+e-1) <- int_of_string (String.sub s ((i-1)*size + !d + r) size) done; if isneg then neg a else a let to_string_pos sgn n = - if Array.length n = 0 then "0" else + if Int.equal (Array.length n) 0 then "0" else sgn ^ String.concat "" (string_of_int n.(0) :: List.map format_size (List.tl (Array.to_list n))) @@ -342,7 +342,7 @@ let mkarray n = t let ints_of_int n = - if n = 0 then [| |] + if Int.equal n 0 then [| |] else if small n then [| n |] else mkarray n @@ -352,7 +352,7 @@ let of_int n = let of_ints n = let n = normalize n in (* TODO: using normalize here seems redundant now *) if n = zero then Obj.repr 0 else - if Array.length n = 1 then Obj.repr n.(0) else + if Int.equal (Array.length n) 1 then Obj.repr n.(0) else Obj.repr n let coerce_to_int = (Obj.magic : Obj.t -> int) @@ -366,7 +366,7 @@ let int_of_ints = let maxi = mkarray max_int and mini = mkarray min_int in fun t -> let l = Array.length t in - if (l > 3) || (l = 3 && (less_than maxi t || less_than t mini)) + if (l > 3) || (Int.equal l 3 && (less_than maxi t || less_than t mini)) then failwith "Bigint.to_int: too large"; let sum = ref 0 in let pow = ref 1 in diff --git a/lib/cArray.ml b/lib/cArray.ml index bdc084f44..4615ad038 100644 --- a/lib/cArray.ml +++ b/lib/cArray.ml @@ -280,8 +280,9 @@ let smartmap f ar = Array.init ar_size copy let map2 f v1 v2 = - if Array.length v1 <> Array.length v2 then invalid_arg "Array.map2"; - if Array.length v1 == 0 then + if not (Int.equal (Array.length v1) (Array.length v2)) then + invalid_arg "Array.map2"; + if Int.equal (Array.length v1) 0 then [| |] else begin let res = Array.create (Array.length v1) (f v1.(0) v2.(0)) in @@ -292,8 +293,9 @@ let map2 f v1 v2 = end let map2_i f v1 v2 = - if Array.length v1 <> Array.length v2 then invalid_arg "Array.map2"; - if Array.length v1 == 0 then + if not (Int.equal (Array.length v1) (Array.length v2)) then + invalid_arg "Array.map2"; + if Int.equal (Array.length v1) 0 then [| |] else begin let res = Array.create (Array.length v1) (f 0 v1.(0) v2.(0)) in @@ -306,7 +308,7 @@ let map2_i f v1 v2 = let map3 f v1 v2 v3 = if Array.length v1 <> Array.length v2 || Array.length v1 <> Array.length v3 then invalid_arg "Array.map3"; - if Array.length v1 == 0 then + if Int.equal (Array.length v1) 0 then [| |] else begin let res = Array.create (Array.length v1) (f v1.(0) v2.(0) v3.(0)) in @@ -318,7 +320,7 @@ let map3 f v1 v2 v3 = let map_left f a = (* Ocaml does not guarantee Array.map is LR *) let l = Array.length a in (* (even if so), then we rewrite it *) - if l = 0 then [||] else begin + if Int.equal l 0 then [||] else begin let r = Array.create l (f a.(0)) in for i = 1 to l - 1 do r.(i) <- f a.(i) @@ -328,7 +330,7 @@ let map_left f a = (* Ocaml does not guarantee Array.map is LR *) let iter2 f v1 v2 = let n = Array.length v1 in - if Array.length v2 <> n then invalid_arg "Array.iter2" + if not (Int.equal (Array.length v2) n) then invalid_arg "Array.iter2" else for i = 0 to n - 1 do f v1.(i) v2.(i) done let pure_functional = false diff --git a/lib/cList.ml b/lib/cList.ml index 62d1ec3c1..ee6b073ea 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -377,7 +377,7 @@ let interval n m = let addn n v = let rec aux n l = - if n = 0 then l + if Int.equal n 0 then l else aux (pred n) (v :: l) in if n < 0 then invalid_arg "List.addn" @@ -525,7 +525,7 @@ let rec remove_assoc_in_triple x = function let rec assoc_snd_in_triple x = function [] -> raise Not_found - | (a,b,_)::l -> if Pervasives.compare a x = 0 then b else assoc_snd_in_triple x l + | (a,b,_)::l -> if Int.equal (Pervasives.compare a x) 0 then b else assoc_snd_in_triple x l let add_set x l = if List.mem x l then l else x :: l @@ -587,7 +587,7 @@ let rec merge_uniq cmp l1 l2 = | l1, [] -> l1 | h1 :: t1, h2 :: t2 -> let c = cmp h1 h2 in - if c = 0 + if Int.equal c 0 then h1 :: merge_uniq cmp t1 t2 else if c <= 0 then h1 :: merge_uniq cmp t1 l2 diff --git a/lib/deque.ml b/lib/deque.ml index 58049b094..335a1a267 100644 --- a/lib/deque.ml +++ b/lib/deque.ml @@ -17,9 +17,9 @@ type 'a t = { let rec split i accu l = match l with | [] -> - if i = 0 then (accu, []) else invalid_arg "split" + if Int.equal i 0 then (accu, []) else invalid_arg "split" | t :: q -> - if i = 0 then (accu, l) + if Int.equal i 0 then (accu, l) else split (pred i) (t :: accu) q let balance q = @@ -88,7 +88,7 @@ let rev q = { let length q = q.lenf + q.lenr -let is_empty q = length q = 0 +let is_empty q = Int.equal (length q) 0 let filter f q = let fold (accu, len) x = if f x then (x :: accu, succ len) else (accu, len) in diff --git a/lib/envars.ml b/lib/envars.ml index b4c72b130..846391d83 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -51,7 +51,7 @@ let expand_path_macros ~warn s = let v = safe_getenv warn (String.sub s (i+1) (n-i-1)) in let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in expand_macros s (i + String.length v) - | '~' when i = 0 -> + | '~' when Int.equal i 0 -> let n = expand_atom s (i+1) in let v = if n=i+1 then home ~warn diff --git a/lib/fmap.ml b/lib/fmap.ml index 8ca56fe7a..21bd4b898 100644 --- a/lib/fmap.ml +++ b/lib/fmap.ml @@ -52,7 +52,7 @@ module Make = functor (X:Map.OrderedType) -> struct Node(Empty, x, data, Empty, 1) | Node(l, v, d, r, h) -> let c = X.compare x v in - if c = 0 then + if Int.equal c 0 then Node(l, x, data, r, h) else if c < 0 then bal (add x data l) v d r @@ -64,7 +64,7 @@ module Make = functor (X:Map.OrderedType) -> struct raise Not_found | Node(l, v, d, r, _) -> let c = X.compare x v in - if c = 0 then d + if Int.equal c 0 then d else find x (if c < 0 then l else r) let rec mem x = function @@ -72,7 +72,7 @@ module Make = functor (X:Map.OrderedType) -> struct false | Node(l, v, d, r, _) -> let c = X.compare x v in - c = 0 || mem x (if c < 0 then l else r) + Int.equal c 0 || mem x (if c < 0 then l else r) let rec min_binding = function Empty -> raise Not_found @@ -97,7 +97,7 @@ module Make = functor (X:Map.OrderedType) -> struct Empty | Node(l, v, d, r, h) -> let c = X.compare x v in - if c = 0 then + if Int.equal c 0 then merge l r else if c < 0 then bal (remove x l) v d r diff --git a/lib/fset.ml b/lib/fset.ml index 567feaa75..c93ce535d 100644 --- a/lib/fset.ml +++ b/lib/fset.ml @@ -93,7 +93,7 @@ struct (Empty, None, Empty) | Node(l, v, r, _) -> let c = X.compare x v in - if c = 0 then (l, Some v, r) + if Int.equal c 0 then (l, Some v, r) else if c < 0 then let (ll, vl, rl) = split x l in (ll, vl, join rl v r) else @@ -109,13 +109,13 @@ struct Empty -> false | Node(l, v, r, _) -> let c = X.compare x v in - c = 0 || mem x (if c < 0 then l else r) + Int.equal c 0 || mem x (if c < 0 then l else r) let rec add x = function Empty -> Node(Empty, x, Empty, 1) | Node(l, v, r, _) as t -> let c = X.compare x v in - if c = 0 then t else + if Int.equal c 0 then t else if c < 0 then bal (add x l) v r else bal l v (add x r) let singleton x = Node(Empty, x, Empty, 1) @@ -124,7 +124,7 @@ struct Empty -> Empty | Node(l, v, r, _) -> let c = X.compare x v in - if c = 0 then merge l r else + if Int.equal c 0 then merge l r else if c < 0 then bal (remove x l) v r else bal l v (remove x r) let rec union s1 s2 = @@ -133,12 +133,12 @@ struct | (t1, Empty) -> t1 | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> if h1 >= h2 then - if h2 = 1 then add v2 s1 else begin + if Int.equal h2 1 then add v2 s1 else begin let (l2, _, r2) = split v1 s2 in join (union l1 l2) v1 (union r1 r2) end else - if h1 = 1 then add v1 s2 else begin + if Int.equal h1 1 then add v1 s2 else begin let (l1, _, r1) = split v2 s1 in join (union l1 l2) v2 (union r1 r2) end @@ -184,7 +184,7 @@ struct compare_aux [s1] [s2] let equal s1 s2 = - compare s1 s2 = 0 + Int.equal (compare s1 s2) 0 let rec subset s1 s2 = match (s1, s2) with @@ -194,7 +194,7 @@ struct false | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) -> let c = X.compare v1 v2 in - if c = 0 then + if Int.equal c 0 then subset l1 l2 && subset r1 r2 else if c < 0 then subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2 diff --git a/lib/gmap.ml b/lib/gmap.ml index 08c99daff..65971b237 100644 --- a/lib/gmap.ml +++ b/lib/gmap.ml @@ -60,7 +60,7 @@ Node(Empty, x, data, Empty, 1) | Node(l, v, d, r, h) -> let c = Pervasives.compare x v in - if c = 0 then + if Int.equal c 0 then Node(l, x, data, r, h) else if c < 0 then bal (add x data l) v d r @@ -72,7 +72,7 @@ raise Not_found | Node(l, v, d, r, _) -> let c = Pervasives.compare x v in - if c = 0 then d + if Int.equal c 0 then d else find x (if c < 0 then l else r) let rec mem x = function @@ -80,7 +80,7 @@ false | Node(l, v, d, r, _) -> let c = Pervasives.compare x v in - c = 0 || mem x (if c < 0 then l else r) + Int.equal c 0 || mem x (if c < 0 then l else r) let rec min_binding = function Empty -> raise Not_found @@ -105,7 +105,7 @@ Empty | Node(l, v, d, r, h) -> let c = Pervasives.compare x v in - if c = 0 then + if Int.equal c 0 then merge l r else if c < 0 then bal (remove x l) v d r @@ -236,7 +236,7 @@ let rec pr_com ft s = Format.pp_print_as ft (utf8_length s1) s1; match os with Some s2 -> - if String.length s2 = 0 then (com_eol := true) + if Int.equal (String.length s2) 0 then (com_eol := true) else (Format.pp_force_newline ft (); pr_com ft s2) | None -> () @@ -441,14 +441,14 @@ let pr_vertical_list pr = function let prvecti_with_sep sep elem v = let rec pr i = - if i = 0 then + if Int.equal i 0 then elem 0 v.(0) else let r = pr (i-1) and s = sep () and e = elem i v.(i) in r ++ s ++ e in let n = Array.length v in - if n = 0 then mt () else pr (n - 1) + if Int.equal n 0 then mt () else pr (n - 1) (* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *) diff --git a/lib/util.ml b/lib/util.ml index 6a0ba470a..84249e6ae 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -65,7 +65,7 @@ let strip s = let string_map f s = let l = String.length s in let r = String.create l in - for i= 0 to (l - 1) do r.[i] <- f (s.[i]) done; + for i = 0 to (l - 1) do r.[i] <- f (s.[i]) done; r let drop_simple_quotes s = @@ -118,7 +118,7 @@ let split_string_at c s = with | Not_found -> [String.sub s n (len-n)] in - if len = 0 then [] else split 0 + if Int.equal len 0 then [] else split 0 let parse_loadpath s = let l = split_string_at '/' s in @@ -207,14 +207,8 @@ let delayed_force f = f () type ('a,'b) union = Inl of 'a | Inr of 'b -module IntOrd = -struct - type t = int - external compare : int -> int -> int = "caml_int_compare" -end - -module Intset = Set.Make(IntOrd) -module Intmap = Map.Make(IntOrd) +module Intset = Set.Make(Int) +module Intmap = Map.Make(Int) (*s interruption *) diff --git a/library/lib.ml b/library/lib.ml index 688df5a0e..212e23578 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -452,7 +452,7 @@ let section_segment_of_mutual_inductive kn = let rec list_mem_assoc x = function | [] -> raise Not_found - | (a,_)::l -> compare a x = 0 or list_mem_assoc x l + | (a, _) :: l -> Int.equal (Names.id_ord a x) 0 || list_mem_assoc x l let section_instance = function | VarRef id -> diff --git a/library/libnames.ml b/library/libnames.ml index 197588f53..a07895eec 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -92,7 +92,7 @@ let sp_ord sp1 sp2 = let (p1,id1) = repr_path sp1 and (p2,id2) = repr_path sp2 in let p_bit = compare p1 p2 in - if p_bit = 0 then id_ord id1 id2 else p_bit + if Int.equal p_bit 0 then id_ord id1 id2 else p_bit module SpOrdered = struct diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 293520a55..dd32c99ba 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -229,9 +229,9 @@ let extend_constr_notation ng = (** Grammar declaration for Tactic Notation (Coq level) *) let get_tactic_entry n = - if n = 0 then + if Int.equal n 0 then weaken_entry Tactic.simple_tactic, None - else if n = 5 then + else if Int.equal n 5 then weaken_entry Tactic.binder_tactic, None else if 1<=n && n<5 then weaken_entry Tactic.tactic_expr, Some (Extend.Level (string_of_int n)) @@ -264,7 +264,7 @@ let head_is_ident tg = match tg.tacgram_prods with let add_tactic_entry tg = let entry, pos = get_tactic_entry tg.tacgram_level in let rules = - if tg.tacgram_level = 0 then begin + if Int.equal tg.tacgram_level 0 then begin if not (head_is_ident tg) then error "Notation for simple tactic must start with an identifier."; let mkact loc l = @@ -293,7 +293,7 @@ let recover_notation_grammar ntn prec = Some (vars, ng) | _ -> None in let l = List.map_filter filter !grammar_state in - assert (List.length l = 1); + let () = match l with [_] -> () | _ -> assert false in List.hd l (* Summary functions: the state of the lexer is included in that of the parser. diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index be584b5c8..3e1c44e5a 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -49,7 +49,7 @@ let rawwit_tactic = function | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n) let tactic_genarg_level s = - if String.length s = 7 && String.sub s 0 6 = "tactic" then + if Int.equal (String.length s) 7 && String.sub s 0 6 = "tactic" then let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48) else None else None diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index a811b29b8..485b5b280 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -227,7 +227,7 @@ let linkmonad f lnkvar = let linklift lnkvar i = linkmonad (fun x -> x+i) lnkvar (* This map is used to deal with debruijn linked indices. *) -module Link = Map.Make (struct type t = int let compare = Pervasives.compare end) +module Link = Map.Make (Int) let pr_links l = Printf.printf "links:\n"; diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index beb7b4819..d42d612ae 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -243,7 +243,7 @@ let rec add_term t0 = function * MODULE: Ordered set of integers. *) -module ISet = Set.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end) +module ISet = Set.Make(Int) (** * Given a set of integers s={i0,...,iN} and a list m, return the list of diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index d9201722d..571c789c2 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -89,7 +89,7 @@ type vector = Vect.t {coeffs = v ; bound = (l,r) } models the constraints l <= v <= r **) -module ISet = Set.Make(struct type t = int let compare = Pervasives.compare end) +module ISet = Set.Make(Int) module PSet = ISet @@ -437,7 +437,7 @@ let elim_var_using_eq vr vect cst prf sys = (** [size sys] computes the number of entries in the system of constraints *) let size sys = System.fold (fun v iref s -> s + (!iref).neg + (!iref).pos) sys 0 -module IMap = Map.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end) +module IMap = Map.Make(Int) let pp_map o map = IMap.fold (fun k elt () -> Printf.fprintf o "%i -> %s\n" k (string_of_num elt)) map () diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index 1f7c083e2..339e10661 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -585,7 +585,7 @@ struct module MonT = struct module MonoMap = Map.Make(Monomial) - module IntMap = Map.Make(struct type t = int let compare = Pervasives.compare end) + module IntMap = Map.Make(Int) (** A hash table might be preferable but requires a hash function. *) let (index_of_monomial : int MonoMap.t ref) = ref (MonoMap.empty) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 7b6be410b..e7300fcea 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -988,7 +988,7 @@ let adjust_predicate_from_tomatch tomatch (current,typ as ct) pb = let rec ungeneralize n ng body = match kind_of_term body with - | Lambda (_,_,c) when ng = 0 -> + | Lambda (_,_,c) when Int.equal ng 0 -> subst1 (mkRel n) c | Lambda (na,t,c) -> (* We traverse an inner generalization *) @@ -1046,8 +1046,8 @@ let rec irrefutable env = function | PatCstr (_,cstr,args,_) -> let ind = inductive_of_constructor cstr in let (_,mip) = Inductive.lookup_mind_specif env ind in - let one_constr = Array.length mip.mind_user_lc = 1 in - one_constr & List.for_all (irrefutable env) args + let one_constr = Int.equal (Array.length mip.mind_user_lc) 1 in + one_constr && List.for_all (irrefutable env) args let first_clause_irrefutable env = function | eqn::mat -> List.for_all (irrefutable env) eqn.patterns @@ -1419,7 +1419,7 @@ let push_binder d (k,env,subst) = let rec list_assoc_in_triple x = function [] -> raise Not_found - | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_in_triple x l + | (a, b, _)::l -> if Int.equal a x then b else list_assoc_in_triple x l (* Let vijk and ti be a set of dependent terms and T a type, all * defined in some environment env. The vijk and ti are supposed to be @@ -1682,7 +1682,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c = let signlen = List.length sign in match kind_of_term tm with | Rel n when dependent tm c - && signlen = 1 (* The term to match is not of a dependent type itself *) -> + && Int.equal signlen 1 (* The term to match is not of a dependent type itself *) -> ((n, len) :: subst, len - signlen) | Rel n when signlen > 1 (* The term is of a dependent type, maybe some variable in its type appears in the tycon. *) -> @@ -2162,7 +2162,7 @@ let build_dependent_signature env evars avoid tomatchs arsign = ([], 0, [], nar, []) tomatchs arsign in let arsign'' = List.rev arsign' in - assert(slift = 0); (* we must have folded over all elements of the arity signature *) + assert(Int.equal slift 0); (* we must have folded over all elements of the arity signature *) arsign'', allnames, nar, eqs, neqs, refls let context_of_arsign l = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index b417dc1d4..405e089a6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -69,7 +69,8 @@ let nfirsts_app_of_stack n s = let (args, _) = strip_app s in List.firstn n args let list_of_app_stack s = let (out,s') = strip_app s in - Option.init (s' = []) out + let init = match s' with [] -> true | _ -> false in + Option.init init out let array_of_app_stack s = Option.map Array.of_list (list_of_app_stack s) let rec zip = function @@ -93,7 +94,7 @@ let rec stack_assign s p c = match s with | _ -> assert false) | _ -> 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 = List.length args in @@ -188,11 +189,11 @@ module RedFlags = (struct let fiota = 16 let fzeta = 32 let mkflags = List.fold_left (lor) 0 - let red_beta f = f land fbeta <> 0 - let red_delta f = f land fdelta <> 0 - let red_eta f = f land feta <> 0 - let red_iota f = f land fiota <> 0 - let red_zeta f = f land fzeta <> 0 + let red_beta f = not (Int.equal (f land fbeta) 0) + let red_delta f = not (Int.equal (f land fdelta) 0) + let red_eta f = not (Int.equal (f land feta) 0) + let red_iota f = not (Int.equal (f land fiota) 0) + let red_zeta f = not (Int.equal (f land fzeta) 0) end : RedFlagsSig) open RedFlags @@ -319,7 +320,7 @@ let rec whd_state_gen flags ts env sigma = match kind_of_term x' with | Rel 1 when l' = empty_stack -> let lc = Array.sub cl 0 (napp-1) in - let u = if napp=1 then f else appvect (f,lc) in + let u = if Int.equal napp 1 then f else appvect (f,lc) in if noccurn 1 u then (pop u,empty_stack) else s | _ -> s else s @@ -375,7 +376,7 @@ let local_whd_state_gen flags sigma = match kind_of_term x' with | Rel 1 when l' = empty_stack -> let lc = Array.sub cl 0 (napp-1) in - let u = if napp=1 then f else appvect (f,lc) in + let u = if Int.equal napp 1 then f else appvect (f,lc) in if noccurn 1 u then (pop u,empty_stack) else s | _ -> s else s @@ -690,7 +691,9 @@ let plain_instance s c = | _ -> map_constr_with_binders succ irec n u in - if s = [] then c else irec 0 c + match s with + | [] -> c + | _ -> irec 0 c (* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota] has (unfortunately) different subtle side effects: @@ -804,7 +807,7 @@ let splay_arity env sigma c = let sort_of_arity env sigma c = snd (splay_arity env sigma c) let splay_prod_n env sigma n = - let rec decrec env m ln c = if m = 0 then (ln,c) else + let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match kind_of_term (whd_betadeltaiota env sigma c) with | Prod (n,a,c0) -> decrec (push_rel (n,None,a) env) @@ -814,7 +817,7 @@ let splay_prod_n env sigma n = decrec env n empty_rel_context let splay_lam_n env sigma n = - let rec decrec env m ln c = if m = 0 then (ln,c) else + let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match kind_of_term (whd_betadeltaiota env sigma c) with | Lambda (n,a,c0) -> decrec (push_rel (n,None,a) env) @@ -941,7 +944,9 @@ let meta_instance sigma b = List.map (fun mv -> (mv,meta_value sigma mv)) (Metaset.elements b.freemetas) in - if c_sigma = [] then b.rebus else instance sigma c_sigma b.rebus + match c_sigma with + | [] -> b.rebus + | _ -> instance sigma c_sigma b.rebus let nf_meta sigma c = meta_instance sigma (mk_freelisted c) @@ -981,7 +986,9 @@ let meta_reducible_instance evd b = with Not_found -> u) | _ -> map_constr irec u in - if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus + match fm with + | [] -> (* nf_betaiota? *) b.rebus + | _ -> irec b.rebus let head_unfold_under_prod ts env _ c = diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 97ce40a77..29d0fa05e 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -959,7 +959,7 @@ let unfold env sigma name = let unfoldoccs env sigma (occs,name) c = let unfo nowhere_except_in locs = let (nbocc,uc) = substlin env name 1 (nowhere_except_in,locs) c in - if nbocc = 1 then + if Int.equal nbocc 1 then error ((string_of_evaluable_ref env name)^" does not occur."); let rest = List.filter (fun o -> o >= nbocc) locs in if rest <> [] then error_invalid_occurrence rest; diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 2585d4489..836997228 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -221,7 +221,7 @@ let lookup_rel_id id sign = | [] -> raise Not_found | (Anonymous, _, _) :: l -> lookrec (n + 1) l | (Name id', b, t) :: l -> - if Names.id_ord id' id = 0 then (n, b, t) else lookrec (n + 1) l + if Int.equal (Names.id_ord id' id) 0 then (n, b, t) else lookrec (n + 1) l in lookrec 1 sign @@ -258,7 +258,7 @@ let rec strip_head_cast c = match kind_of_term c with let rec collapse_rec f cl2 = match kind_of_term f with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) | Cast (c,_,_) -> collapse_rec c cl2 - | _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2) + | _ -> if Int.equal (Array.length cl2) 0 then f else mkApp (f,cl2) in collapse_rec f cl | Cast (c,_,_) -> strip_head_cast c @@ -342,7 +342,7 @@ let fold_rec_types g (lna,typarray,_) e = let map_left2 f a g b = let l = Array.length a in - if l = 0 then [||], [||] else begin + if Int.equal l 0 then [||], [||] else begin let r = Array.create l (f a.(0)) in let s = Array.create l (g b.(0)) in for i = 1 to l - 1 do @@ -911,7 +911,7 @@ let eq_constr = constr_cmp Reduction.CONV let split_app c = match kind_of_term c with App(c,l) -> let len = Array.length l in - if len=0 then ([],c) else + if Int.equal len 0 then ([],c) else let last = Array.get l (len-1) in let prev = Array.sub l 0 (len-1) in c::(Array.to_list prev), last @@ -981,7 +981,7 @@ let rec eta_reduce_head c = (match kind_of_term cl.(lastn) with | Rel 1 -> let c' = - if lastn = 1 then f + if Int.equal lastn 1 then f else mkApp (f, Array.sub cl 0 lastn) in if noccurn 1 c' diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 447ee8e3b..856c5e147 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -395,7 +395,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag let tyN = get_type_of curenv sigma cN in check_compatibility curenv substn tyM tyN); (* Here we check that [cN] does not contain any local variables *) - if nb = 0 then + if Int.equal nb 0 then sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst else if noccur_between 1 nb cN then (sigma, @@ -409,7 +409,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag let tyN = Typing.meta_type sigma k in check_compatibility curenv substn tyM tyN); (* Here we check that [cM] does not contain any local variables *) - if nb = 0 then + if Int.equal nb 0 then (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst) else if noccur_between 1 nb cM then @@ -771,7 +771,7 @@ let merge_instances env sigma flags st1 st2 c1 c2 = let applyHead env evd n c = let rec apprec n c cty evd = - if n = 0 then + if Int.equal n 0 then (evd, c) else match kind_of_term (whd_betadeltaiota env evd cty) with diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 25ea991e7..ebda3cb76 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -321,7 +321,7 @@ let split_product na' = function | _ -> anomaly "ill-formed fixpoint body" let rec split_fix n typ def = - if n = 0 then ([],typ,def) + if Int.equal n 0 then ([],typ,def) else let (na,_,def) = split_lambda def in let (na,t,typ) = split_product na typ in diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 2ec66bb34..26e9f9eb5 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -621,9 +621,10 @@ let pr_fix_tac (id,n,c) = ln nal) [] bll in let idarg,bll = set_nth_name names n bll in - let annot = - if List.length names = 1 then mt() - else spc() ++ str"{struct " ++ pr_id idarg ++ str"}" in + let annot = match names with + | [_] -> mt () + | _ -> spc() ++ str"{struct " ++ pr_id idarg ++ str"}" + in hov 1 (str"(" ++ pr_id id ++ prlist pr_binder_fix bll ++ annot ++ str" :" ++ pr_lconstrarg ty ++ str")") in @@ -973,7 +974,7 @@ in (pr_tac, pr_match_rule) let strip_prod_binders_glob_constr n (ty,_) = let rec strip_ty acc n ty = - if n=0 then (List.rev acc, (ty,None)) else + if Int.equal n 0 then (List.rev acc, (ty,None)) else match ty with Glob_term.GProd(loc,na,Explicit,a,b) -> strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 476504549..721d9b6c8 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -495,7 +495,7 @@ let rec pr_vernac = function | VernacUnfocused -> str"Unfocused" | VernacGoal c -> str"Goal" ++ pr_lconstrarg c | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id - | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i + | VernacUndo i -> if Int.equal i 1 then str"Undo" else str"Undo" ++ pr_intarg i | VernacUndoTo i -> str"Undo" ++ spc() ++ str"To" ++ pr_intarg i | VernacBacktrack (i,j,k) -> str "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k] @@ -523,7 +523,7 @@ let rec pr_vernac = function (* Resetting *) | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id | VernacResetInitial -> str"Reset Initial" - | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i + | VernacBack i -> if Int.equal i 1 then str"Back" else str"Back" ++ pr_intarg i | VernacBackTo i -> str"BackTo" ++ pr_intarg i (* State management *) @@ -634,9 +634,9 @@ let rec pr_vernac = function let pr_constructor_list b l = match l with | Constructors [] -> mt() | Constructors l -> + let fst_sep = match l with [_] -> " " | _ -> " | " in pr_com_at (begin_of_inductive l) ++ - fnl() ++ - str (if List.length l = 1 then " " else " | ") ++ + fnl() ++ str fst_sep ++ prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l | RecordDecl (c,fs) -> spc() ++ diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 5bc3161b9..78bdc194f 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -304,8 +304,8 @@ let tclDO n t = let rec dorec k = if k < 0 then errorlabstrm "Refiner.tclDO" (str"Wrong argument : Do needs a positive integer."); - if k = 0 then tclIDTAC - else if k = 1 then t else (tclTHEN t (dorec (k-1))) + if Int.equal k 0 then tclIDTAC + else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1))) in dorec n @@ -339,7 +339,7 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) (* Repeat on the first subgoal (no failure if no more subgoal) *) let rec tclREPEAT_MAIN t g = - (tclORELSE (tclTHEN_i t (fun i -> if i = 1 then (tclREPEAT_MAIN t) else + (tclORELSE (tclTHEN_i t (fun i -> if Int.equal i 1 then (tclREPEAT_MAIN t) else tclIDTAC)) tclIDTAC) g (*s Tactics handling a list of goals. *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 97c954b8a..8daf11c70 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -77,7 +77,7 @@ type hint_entry = global_reference option * types gen_auto_tactic let pri_order_int (id1, {pri=pri1}) (id2, {pri=pri2}) = let d = pri1 - pri2 in - if d == 0 then id2 - id1 + if Int.equal d 0 then id2 - id1 else d let pri_order t1 t2 = pri_order_int t1 t2 <= 0 diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index e8cde2967..819c76807 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -81,7 +81,7 @@ struct | _ -> Dn.Nothing let bounded_constr_pat_discr_st st (t,depth) = - if depth = 0 then + if Int.equal depth 0 then None else match Term_dn.constr_pat_discr_st st t with @@ -89,7 +89,7 @@ struct | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) let bounded_constr_val_discr_st st (t,depth) = - if depth = 0 then + if Int.equal depth 0 then Dn.Nothing else match constr_val_discr_st st t with @@ -98,7 +98,7 @@ struct | Dn.Everything -> Dn.Everything let bounded_constr_pat_discr (t,depth) = - if depth = 0 then + if Int.equal depth 0 then None else match Term_dn.constr_pat_discr t with @@ -106,7 +106,7 @@ struct | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) let bounded_constr_val_discr (t,depth) = - if depth = 0 then + if Int.equal depth 0 then Dn.Nothing else match constr_val_discr t with diff --git a/tactics/dn.ml b/tactics/dn.ml index a0889ab8f..ea19ecc41 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -16,7 +16,7 @@ struct None,None -> 0 | Some (l,n),Some (l',n') -> let m = Y.compare l l' in - if m = 0 then + if Int.equal m 0 then n-n' else m | Some(l,n),None -> 1 @@ -26,7 +26,7 @@ struct type t = X.t * Z.t let compare (x1,x2) (y1,y2) = let m = (X.compare x1 y1) in - if m = 0 then (Z.compare x2 y2) else + if Int.equal m 0 then (Z.compare x2 y2) else m end @@ -65,7 +65,7 @@ prefix ordering, [dna] is the function returning the main node of a pattern *) try [T.map tm lbl, true] with Not_found -> [] let rec skip_arg n tm = - if n = 0 then [tm,true] + if Int.equal n 0 then [tm,true] else List.flatten (List.map diff --git a/tactics/equality.ml b/tactics/equality.ml index 9827b6146..63cdbfa92 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -296,14 +296,14 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars frze {elimindex = None; elimbody = (elim,NoBindings)} gl let adjust_rewriting_direction args lft2rgt = - if List.length args = 1 then begin + match args with + | [_] -> (* equality to a constant, like in eq_true *) (* more natural to see -> as the rewriting to the constant *) if not lft2rgt then error "Rewriting non-symmetric equality not allowed from right-to-left."; None - end - else + | _ -> (* other equality *) Some lft2rgt @@ -931,7 +931,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let { intro = exist_term } = find_sigma_data sort_of_ty in let evdref = ref (Evd.create_goal_evar_defs sigma) in let rec sigrec_clausal_form siglen p_i = - if siglen = 0 then + if Int.equal siglen 0 then (* is the default value typable with the expected type *) let dflt_typ = type_of env sigma dflt in if Evarconv.e_cumul env evdref dflt_typ p_i then diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 69cee2148..20a52c21c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -179,7 +179,7 @@ let fix_empty_or_and_pattern nv l = let check_or_and_pattern_size loc names n = if List.length names <> n then - if n = 1 then + if Int.equal n 1 then user_err_loc (loc,"",str "Expects a conjunctive pattern.") else user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e55ba5d0e..39c669f42 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1211,7 +1211,7 @@ let keep hyps gl = (************************) let check_number_of_constructors expctdnumopt i nconstr = - if i=0 then error "The constructors are numbered starting from 1."; + if Int.equal i 0 then error "The constructors are numbered starting from 1."; begin match expctdnumopt with | Some n when n <> nconstr -> error ("Not an inductive goal with "^ @@ -1243,7 +1243,7 @@ let any_constructor with_evars tacopt gl = let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in let nconstr = Array.length (snd (Global.lookup_inductive mind)).mind_consnames in - if nconstr = 0 then error "The type has no constructors."; + if Int.equal nconstr 0 then error "The type has no constructors."; tclFIRST (List.map (fun i -> tclTHEN (constructor_tac with_evars None i NoBindings) t) @@ -1286,9 +1286,9 @@ let error_unexpected_extra_pattern loc nb pat = | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no" | _ -> "introduction pattern", "", "none" in user_err_loc (loc,"",str "Unexpected " ++ str s1 ++ str " (" ++ - (if nb = 0 then (str s3 ++ str s2) else + (if Int.equal nb 0 then (str s3 ++ str s2) else (str "at most " ++ int nb ++ str s2)) ++ spc () ++ - str (if nb = 1 then "was" else "were") ++ + str (if Int.equal nb 1 then "was" else "were") ++ strbrk " expected in the branch).") let intro_or_and_pattern loc b ll l' tac id gl = @@ -1297,9 +1297,9 @@ let intro_or_and_pattern loc b ll l' tac id gl = let nv = mis_constr_nargs ind in let bracketed = b or not (l'=[]) in let rec adjust_names_length nb n = function - | [] when n = 0 or not bracketed -> [] + | [] when Int.equal n 0 or not bracketed -> [] | [] -> (dloc,IntroAnonymous) :: adjust_names_length nb (n-1) [] - | (loc',pat) :: _ as l when n = 0 -> + | (loc',pat) :: _ as l when Int.equal n 0 -> if bracketed then error_unexpected_extra_pattern loc' nb pat; l | ip :: l -> ip :: adjust_names_length nb (n-1) l in @@ -2239,7 +2239,7 @@ let empty_scheme = } let make_base n id = - if n=0 or n=1 then id + if Int.equal n 0 || Int.equal n 1 then id else (* This extends the name to accept new digits if it already ends with *) (* digits *) @@ -2260,7 +2260,7 @@ let make_up_names n ind_opt cname = else add_prefix ind_prefix cname in let hyprecname = make_base n base_ind in let avoid = - if n=1 (* Only one recursive argument *) or n=0 then [] + if Int.equal n 1 (* Only one recursive argument *) or Int.equal n 0 then [] else (* Forbid to use cname, cname0, hyprecname and hyprecname0 *) (* in order to get names such as f1, f2, ... *) @@ -2618,13 +2618,15 @@ let decompose_paramspred_branch_args elimt = type (See for example Empty_set_ind, as False would actually be ok). Then we must find the predicate of the conclusion to separate params_pred from args. We suppose there is only one predicate here. *) - if List.length acc2 <> 0 then acc1, acc2 , acc3, ccl - else + match acc2 with + | [] -> let hyps,ccl = decompose_prod_assum elimt in let hd_ccl_pred,_ = decompose_app ccl in - match kind_of_term hd_ccl_pred with + begin match kind_of_term hd_ccl_pred with | Rel i -> let acc3,acc1 = cut_list (i-1) hyps in acc1 , [] , acc3 , ccl | _ -> error_ind_scheme "" + end + | _ -> acc1, acc2 , acc3, ccl let exchange_hd_app subst_hd t = @@ -2694,7 +2696,7 @@ let compute_elim_sig ?elimc elimt = raise Exit end; (* 2- If no args_indargs (=!res.nargs at this point) then no indarg *) - if !res.nargs=0 then raise Exit; + if Int.equal !res.nargs 0 then raise Exit; (* 3- Look at last arg: is it the indarg? *) ignore ( match List.hd args_indargs with @@ -3166,7 +3168,7 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc gl = args *) let induct_destruct isrec with_evars (lc,elim,names,cls) gl = assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *) - if List.length lc = 1 && not (is_functional_induction elim gl) then + if Int.equal (List.length lc) 1 && not (is_functional_induction elim gl) then (* standard induction *) onOpenInductionArg (fun c -> new_induct_gen isrec with_evars elim names c cls) @@ -3182,7 +3184,8 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl = error "'in' clause not supported here."; let lc = List.map (map_induction_arg (pf_apply finish_evar_resolution gl)) lc in - if List.length lc = 1 then + begin match lc with + | [_] -> (* Hook to recover standard induction on non-standard induction schemes *) (* will be removable when is_functional_induction will be more clever *) onInductionArg @@ -3190,7 +3193,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl = if lbind <> NoBindings then error "'with' clause not supported here."; new_induct_gen_l isrec with_evars elim names [c]) (List.hd lc) gl - else + | _ -> let newlc = List.map (fun x -> match x with (* FIXME: should we deal with ElimOnIdent? *) @@ -3198,6 +3201,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl = | _ -> error "Don't know where to find some argument.") lc in new_induct_gen_l isrec with_evars elim names newlc gl + end end let induction_destruct isrec with_evars = function diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml index 2d919e966..4e4b2135d 100644 --- a/toplevel/backtrack.ml +++ b/toplevel/backtrack.ml @@ -146,7 +146,7 @@ let sync nb_opened_proofs = the end. *) let back count = - if count = 0 then 0 + if Int.equal count 0 then 0 else let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in npop count; diff --git a/toplevel/class.ml b/toplevel/class.ml index ff0e9fcfb..87310302c 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -242,7 +242,7 @@ let add_new_coercion_core coef stre source target isid = if coercion_exists coef then raise (CoercionError AlreadyExists); let tg,lp = prods_of t in let llp = List.length lp in - if llp = 0 then raise (CoercionError NotAFunction); + if Int.equal llp 0 then raise (CoercionError NotAFunction); let (cls,lvs,ind) = try get_source lp source diff --git a/toplevel/command.ml b/toplevel/command.ml index edde7c652..f707ea508 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -36,7 +36,7 @@ open Indschemes open Misctypes let rec under_binders env f n c = - if n = 0 then f env Evd.empty c else + if Int.equal n 0 then f env Evd.empty c else match kind_of_term c with | Lambda (x,t,c) -> mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index c0027ef03..b6d1f981c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -312,7 +312,7 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs = let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in let pv = pr_lconstr_env env vargs.(i) in str "The " ++ - (if Array.length vdefj = 1 then mt () else pr_nth (i+1) ++ spc ()) ++ + (if Int.equal (Array.length vdefj) 1 then mt () else pr_nth (i+1) ++ spc ()) ++ str "recursive definition" ++ spc () ++ pvd ++ spc () ++ str "has type" ++ spc () ++ pvdt ++ spc () ++ str "while it should be" ++ spc () ++ pv ++ str "." @@ -809,7 +809,7 @@ let error_ill_formed_inductive env c v = let error_ill_formed_constructor env id c v nparams nargs = let pv = pr_lconstr_env env v in - let atomic = (nb_prod c = 0) in + let atomic = Int.equal (nb_prod c) 0 in str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++ str "is not valid;" ++ brk(1,1) ++ strbrk (if atomic then "it must be " else "its conclusion must be ") ++ @@ -917,8 +917,8 @@ let explain_bad_constructor env cstr ind = str "is expected." let decline_string n s = - if n = 0 then "no "^s^"s" - else if n = 1 then "1 "^s + if Int.equal n 0 then "no "^s^"s" + else if Int.equal n 1 then "1 "^s else (string_of_int n^" "^s^"s") let explain_wrong_numarg_constructor env cstr n = @@ -1020,7 +1020,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c) (List.rev vars @ unboundvars) ++ str ")" else mt())) ++ - (if n=2 then str " (repeated twice)" + (if Int.equal n 2 then str " (repeated twice)" else if n>2 then str " (repeated "++int n++str" times)" else mt()) in if calls <> [] then diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 747f5835f..a49305292 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -292,7 +292,7 @@ let start_proof_with_initialization kind recguard thms snl hook = else tacl)),guard | None -> - assert (List.length thms = 1); + let () = match thms with [_] -> () | _ -> assert false in (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in match thms with | [] -> anomaly "No proof to start" diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index ed6b45228..345147157 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -35,7 +35,7 @@ let cache_token (_,s) = Lexer.add_keyword s let inToken : string -> obj = declare_object {(default_object "TOKEN") with - open_function = (fun i o -> if i=1 then cache_token o); + open_function = (fun i o -> if Int.equal i 1 then cache_token o); cache_function = cache_token; subst_function = Libobject.ident_subst_function; classify_function = (fun o -> Substitute o)} @@ -84,7 +84,7 @@ let classify_tactic_notation tacobj = let inTacticGrammar : tactic_grammar_obj -> obj = declare_object {(default_object "TacticGrammar") with - open_function = (fun i o -> if i=1 then cache_tactic_notation o); + open_function = (fun i o -> if Int.equal i 1 then cache_tactic_notation o); cache_function = cache_tactic_notation; subst_function = subst_tactic_notation; classify_function = classify_tactic_notation} @@ -180,7 +180,7 @@ let parse_format ((loc, str) : lstring) = | cur::l -> (a::cur)::l | [] -> [[a]] in let push_white n l = - if n = 0 then l else push_token (UnpTerminal (String.make n ' ')) l in + if Int.equal n 0 then l else push_token (UnpTerminal (String.make n ' ')) l in let close_box i b = function | a::(_::_ as l) -> push_token (UnpBox (b,a)) l | _ -> error "Non terminated box in format." in @@ -195,7 +195,7 @@ let parse_format ((loc, str) : lstring) = if i < String.length str & str.[i] <> ' ' then if str.[i] = '\'' & quoted & (i+1 >= String.length str or str.[i+1] = ' ') - then if n=0 then error "Empty quoted token." else n + then if Int.equal n 0 then error "Empty quoted token." else n else nonspaces quoted (n+1) (i+1) else if quoted then error "Spaces are not allowed in (quoted) symbols." @@ -240,7 +240,7 @@ let parse_format ((loc, str) : lstring) = push_token (UnpTerminal (String.sub str (i-1) (n+2))) (parse_token (close_quotation (i+n)))) else - if n = 0 then [] + if Int.equal n 0 then [] else error "Ending spaces non part of a format annotation." and parse_box box i = let n = spaces 0 i in @@ -760,7 +760,7 @@ let classify_syntax_definition (local, _ as o) = let inSyntaxExtension : syntax_extension_obj -> obj = declare_object {(default_object "SYNTAX-EXTENSION") with - open_function = (fun i o -> if i = 1 then cache_syntax_extension o); + open_function = (fun i o -> if Int.equal i 1 then cache_syntax_extension o); cache_function = cache_syntax_extension; subst_function = subst_syntax_extension; classify_function = classify_syntax_definition} @@ -1008,7 +1008,7 @@ let open_notation i (_, nobj) = let scope = nobj.notobj_scope in let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in - if i = 1 & not (Notation.exists_notation_in_scope scope ntn pat) then begin + if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin (* Declare the interpretation *) Notation.declare_notation_interpretation ntn scope pat df; (* Declare the uninterpretation *) @@ -1229,7 +1229,7 @@ let load_scope_command _ (_,(scope,dlm)) = Notation.declare_scope scope let open_scope_command i (_,(scope,o)) = - if i=1 then + if Int.equal i 1 then match o with | ScopeDelim dlm -> Notation.declare_delimiters scope dlm | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 6277faf27..5210a3c9e 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -149,7 +149,7 @@ let trunc_named_context n ctx = List.firstn (len - n) ctx let rec chop_product n t = - if n = 0 then Some t + if Int.equal n 0 then Some t else match kind_of_term t with | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None @@ -645,7 +645,7 @@ let get_prog_err n = let get_any_prog_err () = try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id) -let obligations_solved prg = (snd prg.prg_obligations) = 0 +let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0 let all_programs () = ProgMap.fold (fun k p l -> p :: l) !from_prg [] @@ -657,7 +657,7 @@ type progress = let obligations_message rem = if rem > 0 then - if rem = 1 then + if Int.equal rem 1 then Flags.if_verbose msg_info (int rem ++ str " obligation remaining") else Flags.if_verbose msg_info (int rem ++ str " obligations remaining") @@ -898,7 +898,7 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic let info = str (string_of_id n) ++ str " has type-checked" in let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in let obls,_ = prg.prg_obligations in - if Array.length obls = 0 then ( + if Int.equal (Array.length obls) 0 then ( Flags.if_verbose msg_info (info ++ str "."); let cst = declare_definition prg in Defined cst) diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index ec390683f..175a95165 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -56,8 +56,8 @@ let emacs_prompt_endstring() = Printer.emacs_str "</prompt>" beginning of line. *) let prompt_char ic ibuf count = let bol = match ibuf.bols with - | ll::_ -> ibuf.len == ll - | [] -> ibuf.len == 0 + | ll::_ -> Int.equal ibuf.len ll + | [] -> Int.equal ibuf.len 0 in if bol && not !print_emacs then msgerr (str (ibuf.prompt())); try diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7cff9a4ec..42b9411f8 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -170,7 +170,9 @@ let restore_timeout = function let open_utf8_file_in fname = let is_bom s = - Char.code s.[0] = 0xEF && Char.code s.[1] = 0xBB && Char.code s.[2] = 0xBF + Int.equal (Char.code s.[0]) 0xEF && + Int.equal (Char.code s.[1]) 0xBB && + Int.equal (Char.code s.[2]) 0xBF in let in_chan = open_in fname in let s = " " in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 42c36f519..71f7f39a3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -259,7 +259,7 @@ let print_namespace ns = begin match match_dirpath ns dir with | Some [] as y -> y | Some (a::ns') -> - if Names.id_ord a id = 0 then Some ns' + if Int.equal (Names.id_ord a id) 0 then Some ns' else None | None -> None end @@ -272,7 +272,7 @@ let print_namespace ns = begin match match_modulepath ns mp with | Some [] as y -> y | Some (a::ns') -> - if Names.id_ord a id = 0 then Some ns' + if Int.equal (Names.id_ord a id) 0 then Some ns' else None | None -> None end @@ -1551,7 +1551,7 @@ let vernac_undoto n = let vernac_focus gln = let p = Proof_global.give_me_the_proof () in let n = match gln with None -> 1 | Some n -> n in - if n = 0 then + if Int.equal n 0 then Errors.error "Invalid goal number: 0. Goal numbering starts with 1." else Proof.focus focus_command_cond () n p; print_subgoals () |