aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml4
-rw-r--r--pretyping/classops.ml2
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/detyping.ml12
-rw-r--r--pretyping/evarconv.ml6
-rw-r--r--pretyping/evarsolve.ml12
-rw-r--r--pretyping/glob_ops.ml14
-rw-r--r--pretyping/indrec.ml2
-rw-r--r--pretyping/matching.ml2
-rw-r--r--pretyping/namegen.ml8
-rw-r--r--pretyping/patternops.ml16
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--pretyping/recordops.ml2
-rw-r--r--pretyping/redops.ml2
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/retyping.ml2
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--pretyping/termops.ml6
-rw-r--r--pretyping/unification.ml2
19 files changed, 51 insertions, 51 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ade4598e8..72df29e25 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -518,7 +518,7 @@ let dependent_decl a = function
let rec dep_in_tomatch n = function
| (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch n l
- | Abstract (_,d) :: l -> dependent_decl (mkRel n) d or dep_in_tomatch (n+1) l
+ | Abstract (_,d) :: l -> dependent_decl (mkRel n) d || dep_in_tomatch (n+1) l
| [] -> false
let dependencies_in_rhs nargs current tms eqns =
@@ -1356,7 +1356,7 @@ and compile_alias pb (na,orig,(expanded,expanded_typ)) rest =
mkLetIn (na,c,t,j.uj_val);
uj_type = subst1 c j.uj_type } in
let sigma = !(pb.evdref) in
- if not (Flags.is_program_mode ()) && (isRel orig or isVar orig) then
+ if not (Flags.is_program_mode ()) && (isRel orig || isVar orig) then
(* Try to compile first using non expanded alias *)
try f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
with e when precatchable_exception e ->
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 1e1f2184c..06058dfe4 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -82,7 +82,7 @@ module Bijint = struct
type 'a t = { v : (cl_typ * 'a) array; s : int; inv : int ClTypMap.t }
let empty = { v = [||]; s = 0; inv = ClTypMap.empty }
let mem y b = ClTypMap.mem y b.inv
- let map x b = if 0 <= x & x < b.s then b.v.(x) else raise Not_found
+ let map x b = if 0 <= x && x < b.s then b.v.(x) else raise Not_found
let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (b.v.(n)))
let add x y b =
let v =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 93cfdd9be..53fd925a2 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -399,7 +399,7 @@ let inh_coerce_to_prod loc env evd t =
else (evd, t)
let inh_coerce_to_fail env evd rigidonly v t c1 =
- if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
+ if rigidonly && not (Heads.is_rigid env c1 && Heads.is_rigid env t)
then
raise NoCoercion
else
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 1588856f7..7ab2a27ca 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -219,7 +219,7 @@ let lookup_index_as_renamed env t n =
let update_name na ((_,e),c) =
match na with
- | Name _ when force_wildcard () & noccurn (List.index na e) c ->
+ | Name _ when force_wildcard () && noccurn (List.index na e) c ->
Anonymous
| _ ->
na
@@ -250,7 +250,7 @@ and align_tree nal isgoal (e,c as rhs) = match nal with
| na::nal ->
match kind_of_term c with
| Case (ci,p,c,cl) when eq_constr c (mkRel (List.index na (snd e)))
- & (* don't contract if p dependent *)
+ && (* don't contract if p dependent *)
computable p (ci.ci_pp_info.ind_nargs) ->
let clauses = build_tree na isgoal e ci cl in
List.flatten
@@ -502,7 +502,7 @@ and share_names isgoal n l avoid env c t =
and detype_eqns isgoal avoid env ci computable constructs consnargsl bl =
try
- if !Flags.raw_print or not (reverse_matching ()) then raise Exit;
+ if !Flags.raw_print || not (reverse_matching ()) then raise Exit;
let mat = build_tree Anonymous isgoal (avoid,env) ci bl in
List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env c))
mat
@@ -512,7 +512,7 @@ and detype_eqns isgoal avoid env ci computable constructs consnargsl bl =
and detype_eqn isgoal avoid env constr construct_nargs branch =
let make_pat x avoid env b ids =
- if force_wildcard () & noccurn 1 b then
+ if force_wildcard () && noccurn 1 b then
PatVar (dl,Anonymous),avoid,(add_name Anonymous env),ids
else
let id = next_name_away_in_cases_pattern x avoid in
@@ -656,7 +656,7 @@ let rec subst_glob_constr subst raw =
and b1' = subst_glob_constr subst b1
and b2' = subst_glob_constr subst b2
and c' = subst_glob_constr subst c in
- if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else
+ if c' == c && po' == po && b1' == b1 && b2' == b2 then raw else
GIf (loc,c',(na,po'),b1',b2')
| GRec (loc,fix,ida,bl,ra1,ra2) ->
@@ -666,7 +666,7 @@ let rec subst_glob_constr subst raw =
(List.smartmap (fun (na,k,obd,ty as dcl) ->
let ty' = subst_glob_constr subst ty in
let obd' = Option.smartmap (subst_glob_constr subst) obd in
- if ty'==ty & obd'==obd then dcl else (na,k,obd',ty')))
+ if ty'==ty && obd'==obd then dcl else (na,k,obd',ty')))
bl in
if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
GRec (loc,fix,ida,bl',ra1',ra2')
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6d4f214cc..ded8314dd 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -442,7 +442,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
ise_try evd [f1; f2; f3]
end
- | Rigid, Rigid when isLambda term1 & isLambda term2 ->
+ | Rigid, Rigid when isLambda term1 && isLambda term2 ->
let (na,c1,c'1) = destLambda term1 in
let (_,c2,c'2) = destLambda term2 in
assert app_empty;
@@ -790,7 +790,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
let app_empty = match l1, l2 with [], [] -> true | _ -> false in
match kind_of_term term1, kind_of_term term2 with
| Evar (evk1,args1), (Rel _|Var _) when app_empty
- & List.for_all (fun a -> eq_constr a term2 or isEvar a)
+ && List.for_all (fun a -> eq_constr a term2 || isEvar a)
(remove_instance_local_defs evd evk1 (Array.to_list args1)) ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
@@ -798,7 +798,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
| Some evd -> Success evd
| None -> UnifFailure (evd, ConversionFailed (env,term1,term2)))
| (Rel _|Var _), Evar (evk2,args2) when app_empty
- & List.for_all (fun a -> eq_constr a term1 or isEvar a)
+ && List.for_all (fun a -> eq_constr a term1 || isEvar a)
(remove_instance_local_defs evd evk2 (Array.to_list args2)) ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index a1bf6eabb..df0187f73 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -185,7 +185,7 @@ let get_alias_chain_of aliases x = match kind_of_term x with
let normalize_alias_opt aliases x =
match get_alias_chain_of aliases x with
| [] -> None
- | a::_ when isRel a or isVar a -> Some a
+ | a::_ when isRel a || isVar a -> Some a
| [_] -> None
| _::a::_ -> Some a
@@ -280,9 +280,9 @@ let free_vars_and_rels_up_alias_expansion aliases c =
let rec expand_and_check_vars aliases = function
| [] -> []
- | a::l when isRel a or isVar a ->
+ | a::l when isRel a || isVar a ->
let a = expansion_of_var aliases a in
- if isRel a or isVar a then a :: expand_and_check_vars aliases l
+ if isRel a || isVar a then a :: expand_and_check_vars aliases l
else raise Exit
| _ ->
raise Exit
@@ -346,7 +346,7 @@ let is_unification_pattern_meta env nb m l t =
None
let is_unification_pattern_evar env evd (evk,args) l t =
- if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar env evd evk t
+ if List.for_all (fun x -> isRel x || isVar x) l && noccur_evar env evd evk t
then
let args = remove_instance_local_defs evd evk (Array.to_list args) in
let n = List.length args in
@@ -1167,7 +1167,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
let (evd,evar,(evk',argsv' as ev')) =
materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in
let ts = expansions_of_var aliases t in
- let test c = isEvar c or List.mem c ts in
+ let test c = isEvar c || List.mem c ts in
let filter =
restrict_upon_filter evd evk test (Array.to_list argsv') in
let filter = closure_of_filter evd evk' filter in
@@ -1355,7 +1355,7 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
*)
let status_changed lev (pbty,_,t1,t2) =
- (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) or
+ (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) ||
(try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false)
let reconsider_conv_pbs conv_algo evd =
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index e219bbeb1..88702b350 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -126,7 +126,7 @@ let same_id na id = match na with
let occur_glob_constr id =
let rec occur = function
| GVar (loc,id') -> Id.equal id id'
- | GApp (loc,f,args) -> (occur f) or (List.exists occur args)
+ | GApp (loc,f,args) -> (occur f) || (List.exists occur args)
| GLambda (loc,na,bk,ty,c) ->
(occur ty) || (not (same_id na id) && (occur c))
| GProd (loc,na,bk,ty,c) ->
@@ -135,13 +135,13 @@ let occur_glob_constr id =
(occur b) || (not (same_id na id) && (occur c))
| GCases (loc,sty,rtntypopt,tml,pl) ->
(occur_option rtntypopt)
- or (List.exists (fun (tm,_) -> occur tm) tml)
- or (List.exists occur_pattern pl)
+ || (List.exists (fun (tm,_) -> occur tm) tml)
+ || (List.exists occur_pattern pl)
| GLetTuple (loc,nal,rtntyp,b,c) ->
occur_return_type rtntyp id
- or (occur b) or (not (List.mem (Name id) nal) & (occur c))
+ || (occur b) || (not (List.mem (Name id) nal) && (occur c))
| GIf (loc,c,rtntyp,b1,b2) ->
- occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
+ occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2)
| GRec (loc,fk,idl,bl,tyl,bv) ->
not (Array.for_all4 (fun fid bl ty bd ->
let rec occur_fix = function
@@ -154,11 +154,11 @@ let occur_glob_constr id =
(match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in
occur_fix bl)
idl bl tyl bv)
- | GCast (loc,c,k) -> (occur c) or (match k with CastConv t
+ | GCast (loc,c,k) -> (occur c) || (match k with CastConv t
| CastVM t | CastNative t -> occur t | CastCoerce -> false)
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false
- and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)
+ and occur_pattern (loc,idl,p,c) = not (List.mem id idl) && (occur c)
and occur_option = function None -> false | Some p -> occur p
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index fa7b954d9..23996282c 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -172,7 +172,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
let nP = lift (i+1+decP) p in
let env' = push_rel (n,None,t) env in
let t_0 = process_pos env' dep' nP (lift 1 t) in
- make_prod_dep (dep or dep') env
+ make_prod_dep (dep || dep') env
(n,t,
mkArrow t_0
(process_constr
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 65971d6e3..16a9c8a32 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -213,7 +213,7 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in
let n = rel_context_length ctx in
let n' = rel_context_length ctx' in
- if noccur_between 1 n b2 & noccur_between 1 n' b2' then
+ if noccur_between 1 n b2 && noccur_between 1 n' b2' then
let s =
List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx in
let s' =
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 1736bcff2..bf0d7b879 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -161,7 +161,7 @@ let restart_subscript id =
let next_name_away_in_cases_pattern na avoid =
let id = match na with Name id -> id | Anonymous -> default_x in
- next_ident_away_from id (fun id -> List.mem id avoid or is_constructor id)
+ next_ident_away_from id (fun id -> List.mem id avoid || is_constructor id)
(* 2- Looks for a fresh name for introduction in goal *)
@@ -174,7 +174,7 @@ let next_name_away_in_cases_pattern na avoid =
let next_ident_away_in_goal id avoid =
let id = if List.mem id avoid then restart_subscript id else id in
- let bad id = List.mem id avoid || (is_global id & not (is_section_variable id)) in
+ let bad id = List.mem id avoid || (is_global id && not (is_section_variable id)) in
next_ident_away_from id bad
let next_name_away_in_goal na avoid =
@@ -248,7 +248,7 @@ let visibly_occur_id id (nenv,c) =
let short = shortest_qualid_of_global Id.Set.empty (global_of_constr c) in
qualid_eq short (qualid_of_ident id) ->
raise Occur
- | Rel p when p>n & occur_rel (p-n) nenv id -> raise Occur
+ | Rel p when p>n && occur_rel (p-n) nenv id -> raise Occur
| _ -> iter_constr_with_binders succ occur n c
in
try occur 1 c; false
@@ -256,7 +256,7 @@ let visibly_occur_id id (nenv,c) =
| Not_found -> false (* Happens when a global is not in the env *)
let next_ident_away_for_default_printing env_t id avoid =
- let bad id = List.mem id avoid or visibly_occur_id id env_t in
+ let bad id = List.mem id avoid || visibly_occur_id id env_t in
next_ident_away_from id bad
let next_name_away_for_default_printing env_t na avoid =
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b80484599..e6a95a03e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -80,16 +80,16 @@ and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
let rec occur_meta_pattern = function
| PApp (f,args) ->
- (occur_meta_pattern f) or (Array.exists occur_meta_pattern args)
- | PLambda (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c)
- | PProd (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c)
- | PLetIn (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c)
+ (occur_meta_pattern f) || (Array.exists occur_meta_pattern args)
+ | PLambda (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c)
+ | PProd (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c)
+ | PLetIn (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c)
| PIf (c,c1,c2) ->
- (occur_meta_pattern c) or
- (occur_meta_pattern c1) or (occur_meta_pattern c2)
+ (occur_meta_pattern c) ||
+ (occur_meta_pattern c1) || (occur_meta_pattern c2)
| PCase(_,p,c,br) ->
- (occur_meta_pattern p) or
- (occur_meta_pattern c) or
+ (occur_meta_pattern p) ||
+ (occur_meta_pattern c) ||
(List.exists (fun (_,_,p) -> occur_meta_pattern p) br)
| PMeta _ | PSoApp _ -> true
| PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 265ba4b14..05968b6be 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -471,7 +471,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
let f = whd_evar !evdref f in
begin match kind_of_term f with
| Ind _ | Const _
- when isInd f or has_polymorphic_type (destConst f)
+ when isInd f || has_polymorphic_type (destConst f)
->
let sigma = !evdref in
let c = mkApp (f,Array.map (whd_evar sigma) args) in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index eaf7bf0aa..94119975a 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -243,7 +243,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) =
(* the first component of subst_con. *)
let cst' = fst (subst_con subst cst) in
let ind' = Inductiveops.subst_inductive subst ind in
- if cst' == cst & ind' == ind then obj else (cst',ind')
+ if cst' == cst && ind' == ind then obj else (cst',ind')
let discharge_canonical_structure (_,(cst,ind)) =
Some (Lib.discharge_con cst,Lib.discharge_inductive ind)
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
index 46f668476..1713a371e 100644
--- a/pretyping/redops.ml
+++ b/pretyping/redops.ml
@@ -20,7 +20,7 @@ let make_red_flag l =
"Cannot set both constants to unfold and constants not to unfold";
add_flag { red with rConst = Util.List.union red.rConst l } lf
| FDeltaBut l :: lf ->
- if red.rConst <> [] & not red.rDelta then
+ if red.rConst <> [] && not red.rDelta then
Errors.error
"Cannot set both constants to unfold and constants not to unfold";
add_flag
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index ad5f5a7ae..3860cc015 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -353,7 +353,7 @@ let contract_fix ?env ((recindices,bodynum),(names,types,bodies as typedbodies))
substl closure bodies.(bodynum)
let fix_recarg ((recindices,bodynum),_) stack =
- assert (0 <= bodynum & bodynum < Array.length recindices);
+ assert (0 <= bodynum && bodynum < Array.length recindices);
let recargnum = Array.get recindices bodynum in
try
Some (recargnum, stack_nth stack recargnum)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index f5f977615..170e21a90 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -163,7 +163,7 @@ let retype ?(polyprop=true) sigma =
| Prod (name,t,c2) ->
let s2 = sort_family_of (push_rel (name,None,t) env) c2 in
if not (is_impredicative_set env) &&
- s2 == InSet & sort_family_of env t == InType then InType else s2
+ s2 == InSet && sort_family_of env t == InType then InType else s2
| App(f,args) when isGlobalRef f ->
let t = type_of_global_reference_knowing_parameters env f args in
family_of_sort (sort_of_atomic_type env sigma t args)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index c7c869d63..fc9f087fd 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -883,7 +883,7 @@ let contextually byhead (occs,c) f env sigma t =
let maxocc = List.fold_right max locs 0 in
let pos = ref 1 in
let rec traverse (env,c as envc) t =
- if nowhere_except_in & (!pos > maxocc) then t
+ if nowhere_except_in && (!pos > maxocc) then t
else
try
let subst = if byhead then matches_head c t else matches c t in
@@ -920,7 +920,7 @@ let substlin env evalref n (nowhere_except_in,locs) c =
let value = value_of_evaluable_ref env evalref in
let term = constr_of_evaluable_ref evalref in
let rec substrec () c =
- if nowhere_except_in & !pos > maxocc then c
+ if nowhere_except_in && !pos > maxocc then c
else if eq_constr c term then
let ok =
if nowhere_except_in then List.mem !pos locs
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 81270b5f7..66a656ad7 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -582,7 +582,7 @@ let dependent_main noevar m t =
Array.iter (deprec m)
(Array.sub lt
(Array.length lm) ((Array.length lt) - (Array.length lm)))
- | _, Cast (c,_,_) when noevar & isMeta c -> ()
+ | _, Cast (c,_,_) when noevar && isMeta c -> ()
| _, Evar _ when noevar -> ()
| _ -> iter_constr_with_binders (lift 1) deprec m t
in
@@ -742,7 +742,7 @@ let subst_closed_term_occ_gen_modulo occs test cl occ t =
let lastpos = Option.get test.last_found in
error_cannot_unify_occurrences !nested (cl,!pos,t) lastpos in
let rec substrec k t =
- if nowhere_except_in & !pos > maxocc then t else
+ if nowhere_except_in && !pos > maxocc then t else
try
let subst = test.match_fun t in
if Locusops.is_selected !pos occs then
@@ -894,7 +894,7 @@ let compare_constr_univ f cv_pb t1 t2 =
match kind_of_term t1, kind_of_term t2 with
Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
| Prod (_,t1,c1), Prod (_,t2,c2) ->
- f Reduction.CONV t1 t2 & f cv_pb c1 c2
+ f Reduction.CONV t1 t2 && f cv_pb c1 c2
| _ -> compare_constr (f Reduction.CONV) t1 t2
let rec constr_cmp cv_pb t1 t2 = compare_constr_univ constr_cmp cv_pb t1 t2
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4f6741d87..003b57693 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1167,7 +1167,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
List.exists (fun op -> eq_constr op cl) l
then error_non_linear_unification env evd hdmeta cl
else (evd',cl::l)
- else if flags.allow_K_in_toplevel_higher_order_unification or dependent op t
+ else if flags.allow_K_in_toplevel_higher_order_unification || dependent op t
then
(evd,op::l)
else
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 06:25:35 +0000