Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Monomorphized a lot of equalities over OCaml integers, thanks to

the new Int module. Only the most obvious were removed, so there
are a lot more in the wild.

This may sound heavyweight, but it has two advantages:

1. Monomorphization is explicit, hence we do not miss particular
optimizations of equality when doing it carelessly with the generic
equality.

2. When we have removed all the generic equalities on integers, we
will be able to write something like "let (=) = ()" to retrieve all
its other uses (mostly faulty) spread throughout the code, statically.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit b0b1710ba631f3a3a3faad6e955ef703c67cb967 1 parent bafb198
Pierre-Marie Pédrot ppedrot authored
Showing with 276 additions and 259 deletions.
  1. +3 −3 interp/constrextern.ml
  2. +3 −3 interp/constrintern.ml
  3. +2 −2 interp/notation_ops.ml
  4. +12 −12 kernel/cbytegen.ml
  5. +3 −3 kernel/cemitcodes.ml
  6. +4 −4 kernel/closure.ml
  7. +1 −1  kernel/environ.ml
  8. +6 −6 kernel/esubst.ml
  9. +4 −4 kernel/indtypes.ml
  10. +2 −2 kernel/inductive.ml
  11. +34 −30 kernel/names.ml
  12. +2 −2 kernel/reduction.ml
  13. +4 −4 kernel/subtyping.ml
  14. +11 −8 kernel/term.ml
  15. +2 −2 kernel/univ.ml
  16. +5 −5 kernel/vm.ml
  17. +17 −17 lib/bigint.ml
  18. +9 −7 lib/cArray.ml
  19. +3 −3 lib/cList.ml
  20. +3 −3 lib/deque.ml
  21. +1 −1  lib/envars.ml
  22. +4 −4 lib/fmap.ml
  23. +8 −8 lib/fset.ml
  24. +4 −4 lib/gmap.ml
  25. +3 −3 lib/pp.ml
  26. +4 −10 lib/util.ml
  27. +1 −1  library/lib.ml
  28. +1 −1  library/libnames.ml
  29. +4 −4 parsing/egramcoq.ml
  30. +1 −1  parsing/extrawit.ml
  31. +1 −1  plugins/funind/merge.ml
  32. +1 −1  plugins/micromega/coq_micromega.ml
  33. +2 −2 plugins/micromega/mfourier.ml
  34. +1 −1  plugins/micromega/polynomial.ml
  35. +6 −6 pretyping/cases.ml
  36. +21 −14 pretyping/reductionops.ml
  37. +1 −1  pretyping/tacred.ml
  38. +5 −5 pretyping/termops.ml
  39. +3 −3 pretyping/unification.ml
  40. +1 −1  printing/ppconstr.ml
  41. +5 −4 printing/pptactic.ml
  42. +4 −4 printing/ppvernac.ml
  43. +3 −3 proofs/refiner.ml
  44. +1 −1  tactics/auto.ml
  45. +4 −4 tactics/btermdn.ml
  46. +3 −3 tactics/dn.ml
  47. +4 −4 tactics/equality.ml
  48. +1 −1  tactics/tacticals.ml
  49. +19 −15 tactics/tactics.ml
  50. +1 −1  toplevel/backtrack.ml
  51. +1 −1  toplevel/class.ml
  52. +1 −1  toplevel/command.ml
  53. +5 −5 toplevel/himsg.ml
  54. +1 −1  toplevel/lemmas.ml
  55. +8 −8 toplevel/metasyntax.ml
  56. +4 −4 toplevel/obligations.ml
  57. +2 −2 toplevel/toplevel.ml
  58. +3 −1 toplevel/vernac.ml
  59. +3 −3 toplevel/vernacentries.ml
6 interp/constrextern.ml
View
@@ -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
6 interp/constrintern.ml
View
@@ -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
4 interp/notation_ops.ml
View
@@ -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
24 kernel/cbytegen.ml
View
@@ -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)
6 kernel/cemitcodes.ml
View
@@ -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
8 kernel/closure.ml
View
@@ -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
2  kernel/environ.ml
View
@@ -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
12 kernel/esubst.ml
View
@@ -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
8 kernel/indtypes.ml
View
@@ -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
4 kernel/inductive.ml
View
@@ -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
64 kernel/names.ml
View
@@ -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
4 kernel/reduction.ml
View
@@ -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
8 kernel/subtyping.ml
View
@@ -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
19 kernel/term.ml
View
@@ -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
4 kernel/univ.ml
View
@@ -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
10 kernel/vm.ml
View
@@ -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
34 lib/bigint.ml
View
@@ -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
16 lib/cArray.ml
View
@@ -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
6 lib/cList.ml
View
@@ -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
6 lib/deque.ml
View
@@ -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
2  lib/envars.ml
View
@@ -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
8 lib/fmap.ml
View
@@ -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
16 lib/fset.ml
View
@@ -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
8 lib/gmap.ml
View
@@ -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
6 lib/pp.ml
View
@@ -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] *)
14 lib/util.ml
View
@@ -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 *)
2  library/lib.ml
View
@@ -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 ->
2  library/libnames.ml
View
@@ -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
8 parsing/egramcoq.ml
View
@@ -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.
2  parsing/extrawit.ml
View
@@ -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
2  plugins/funind/merge.ml
View
@@ -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";
2  plugins/micromega/coq_micromega.ml
View
@@ -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
4 plugins/micromega/mfourier.ml
View
@@ -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 ()
2  plugins/micromega/polynomial.ml
View
@@ -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)
12 pretyping/cases.ml
View
@@ -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 =
35 pretyping/reductionops.ml
View
@@ -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 =
2  pretyping/tacred.ml
View
@@ -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;
10 pretyping/termops.ml
View
@@ -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'
6 pretyping/unification.ml
View
@@ -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
2  printing/ppconstr.ml
View
@@ -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
9 printing/pptactic.ml
View
@@ -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
8 printing/ppvernac.ml
View
@@ -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() ++
6 proofs/refiner.ml
View
@@ -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. *)
2  tactics/auto.ml
View
@@ -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
8 tactics/btermdn.ml
View
@@ -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
6 tactics/dn.ml
View
@@ -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
8 tactics/equality.ml
View
@@ -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
2  tactics/tacticals.ml
View
@@ -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
34 tactics/tactics.ml
View
@@ -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
2  toplevel/backtrack.ml
View
@@ -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;
2  toplevel/class.ml
View
@@ -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
2  toplevel/command.ml
View
@@ -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)
10 toplevel/himsg.ml
View