Get rid of the uses of deprecated OCaml elements (still remaining compatible with OCaml 3.12.1).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7

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