aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml12
-rw-r--r--pretyping/reductionops.ml35
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/termops.ml10
-rw-r--r--pretyping/unification.ml6
5 files changed, 36 insertions, 29 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7b6be410b9..e7300fceaf 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 b417dc1d48..405e089a68 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 97ce40a77b..29d0fa05e7 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 2585d44898..8369972284 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 447ee8e3bb..856c5e1477 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-11-03 16:48:39 +0000