diff options
76 files changed, 243 insertions, 243 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 7ba861704..741ef9853 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -282,7 +282,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, []) | _ -> try - if !Flags.raw_print or !print_no_symbol then raise No_match; + if !Flags.raw_print || !print_no_symbol then raise No_match; let (na,sc,p) = uninterp_prim_token_cases_pattern pat in match availability_of_prim_token p sc scopes with | None -> raise No_match @@ -291,7 +291,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na with No_match -> try - if !Flags.raw_print or !print_no_symbol then raise No_match; + if !Flags.raw_print || !print_no_symbol then raise No_match; extern_symbol_pattern scopes vars pat (uninterp_cases_pattern_notations pat) with No_match -> @@ -409,7 +409,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = CPatCstr (Loc.ghost, c, add_patt_for_params ind args, []) else try - if !Flags.raw_print or !print_no_symbol then raise No_match; + if !Flags.raw_print || !print_no_symbol then raise No_match; let (sc,p) = uninterp_prim_token_ind_pattern ind args in match availability_of_prim_token p sc scopes with | None -> raise No_match @@ -417,7 +417,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = insert_pat_delimiters Loc.ghost (CPatPrim(Loc.ghost,p)) key with No_match -> try - if !Flags.raw_print or !print_no_symbol then raise No_match; + if !Flags.raw_print || !print_no_symbol then raise No_match; extern_symbol_ind_pattern scopes vars ind args (uninterp_ind_pattern_notations ind) with No_match -> @@ -439,7 +439,7 @@ let occur_name na aty = | Anonymous -> false let is_projection nargs = function - | Some r when not !Flags.raw_print & !print_projections -> + | Some r when not !Flags.raw_print && !print_projections -> (try let n = Recordops.find_projection_nparams r + 1 in if n <= nargs then Some n else None @@ -463,11 +463,11 @@ let explicitize loc inctx impl (cf,f) args = | a::args, imp::impl when is_status_implicit imp -> let tail = exprec (q+1) (args,impl) in let visible = - !Flags.raw_print or - (!print_implicits & !print_implicits_explicit_args) or - (is_needed_for_correct_partial_application tail imp) or - (!print_implicits_defensive & - is_significant_implicit a & + !Flags.raw_print || + (!print_implicits && !print_implicits_explicit_args) || + (is_needed_for_correct_partial_application tail imp) || + (!print_implicits_defensive && + is_significant_implicit a && not (is_inferable_implicit inctx n imp)) in if visible then @@ -506,7 +506,7 @@ let extern_app loc inctx impl (cf,f) args = CAppExpl (loc, (None, f), []) else if not !Constrintern.parsing_explicit && ((!Flags.raw_print || - (!print_implicits & not !print_implicits_explicit_args)) & + (!print_implicits && not !print_implicits_explicit_args)) && List.exists is_status_implicit impl) then CAppExpl (loc, (is_projection (List.length args) cf, f), args) @@ -524,11 +524,11 @@ let rec extern_args extern scopes env args subscopes = let rec remove_coercions inctx = function | GApp (loc,GRef (_,r),args) as c - when not (!Flags.raw_print or !print_coercions) + when not (!Flags.raw_print || !print_coercions) -> let nargs = List.length args in (try match Classops.hide_coercion r with - | Some n when n < nargs && (inctx or n+1 < nargs) -> + | Some n when n < nargs && (inctx || n+1 < nargs) -> (* We skip a coercion *) let l = List.skipn n args in let (a,l) = match l with a::l -> (a,l) | [] -> assert false in @@ -583,12 +583,12 @@ let extern_glob_sort = function let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try - if !Flags.raw_print or !print_no_symbol then raise No_match; + if !Flags.raw_print || !print_no_symbol then raise No_match; extern_optimal_prim_token scopes r r' with No_match -> try let r'' = flatten_application r' in - if !Flags.raw_print or !print_no_symbol then raise No_match; + if !Flags.raw_print || !print_no_symbol then raise No_match; extern_symbol scopes vars r'' (uninterp_notations r'') with No_match -> match r' with | GRef (loc,ref) -> @@ -764,7 +764,7 @@ and factorize_prod scopes vars na bk aty c = match na, c with | Name id, CProdN (loc,[nal,Default bk',ty],c) when binding_kind_eq bk bk' && constr_expr_eq aty ty - & not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> + && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> nal,c | _ -> [],c @@ -774,7 +774,7 @@ and factorize_lambda inctx scopes vars na bk aty c = match c with | CLambdaN (loc,[nal,Default bk',ty],c) when binding_kind_eq bk bk' && constr_expr_eq aty ty - & not (occur_name na ty) (* avoid na in ty escapes scope *) -> + && not (occur_name na ty) (* avoid na in ty escapes scope *) -> nal,c | _ -> [],c @@ -791,7 +791,7 @@ and extern_local_binder scopes vars = function let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with (assums,ids,LocalRawAssum(nal,k,ty')::l) - when constr_expr_eq ty ty' & + when constr_expr_eq ty ty' && match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ece2a4518..51c8e2e10 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -630,7 +630,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = GVar (loc,id), make_implicits_list impls, argsc, expl_impls with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) - if Id.Set.mem id genv.ids or Id.Set.mem id ltacvars + if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars then GVar (loc,id), [], [], [] (* Is [id] a notation variable *) diff --git a/interp/notation.ml b/interp/notation.ml index 624fa23aa..a04631580 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -832,7 +832,7 @@ let browse_notation strict ntn map = let global_reference_of_notation test (ntn,(sc,c,_)) = match c with | NRef ref when test ref -> Some (ntn,sc,ref) - | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l & test ref -> + | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l && test ref -> Some (ntn,sc,ref) | _ -> None diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index b571d0344..0e4cd80df 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -151,14 +151,14 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> - on_true_do (f ty1 ty2 & f c1 c2) add na1 + on_true_do (f ty1 ty2 && f c1 c2) add na1 | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> - on_true_do (f ty1 ty2 & f c1 c2) add na1 + on_true_do (f ty1 ty2 && f c1 c2) add na1 | GHole _, GHole _ -> true | GSort (_,s1), GSort (_,s2) -> glob_sort_eq s1 s2 | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 -> - on_true_do (f b1 b2 & f c1 c2) add na1 + on_true_do (f b1 b2 && f c1 c2) add na1 | (GCases _ | GRec _ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ | _,(GCases _ | GRec _ @@ -315,8 +315,8 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) = let () = List.iter check foundrecbinding in let check_bound x = if not (List.mem x found) then - if List.mem_assoc x foundrec or List.mem_assoc x foundrecbinding - or list_rev_mem_assoc x foundrec or list_rev_mem_assoc x foundrecbinding + if List.mem_assoc x foundrec || List.mem_assoc x foundrecbinding + || list_rev_mem_assoc x foundrec || list_rev_mem_assoc x foundrecbinding then error ((Id.to_string x)^" should not be bound in a recursive pattern of the right-hand side.") else @@ -424,7 +424,7 @@ let rec subst_notation_constr subst bound raw = (cpl',r')) branches in - if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' & + if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' && rl' == rl && branches' == branches then raw else NCases (sty,rtntypopt',rl',branches') diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 43c79bd49..832af5331 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -264,7 +264,7 @@ let locs_of_notation loc locs ntn = let rec aux pos = function | [] -> if Int.equal pos el then [] else [(pos,el-1)] | (ba,ea)::l ->if Int.equal pos ba then aux ea l else (pos,ba-1)::aux ea l - in aux bl (Sort.list (fun l1 l2 -> fst l1 < fst l2) locs) + in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs) let ntn_loc loc (args,argslist,binderslist) = locs_of_notation loc diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 532f57866..2b9ca425f 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -96,7 +96,7 @@ let label_table = ref ([| |] : label_definition array) let extend_label_table needed = let new_size = ref(Array.length !label_table) in while needed >= !new_size do new_size := 2 * !new_size done; - let new_table = Array.create !new_size (Label_undefined []) in + let new_table = Array.make !new_size (Label_undefined []) in Array.blit !label_table 0 new_table 0 (Array.length !label_table); label_table := new_table @@ -304,7 +304,7 @@ let rec emit = function let init () = out_position := 0; - label_table := Array.create 16 (Label_undefined []); + label_table := Array.make 16 (Label_undefined []); reloc_info := [] type emitcodes = string diff --git a/kernel/closure.ml b/kernel/closure.ml index 49fd1ae8e..faa67be46 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -669,11 +669,11 @@ let rec to_constr constr_fun lfts v = let term_of_fconstr = let rec term_of_fconstr_lift lfts v = match v.term with - | FCLOS(t,env) when is_subs_id env & is_lift_id lfts -> t - | FLambda(_,tys,f,e) when is_subs_id e & is_lift_id lfts -> + | FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t + | FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts -> compose_lam (List.rev tys) f - | FFix(fx,e) when is_subs_id e & is_lift_id lfts -> mkFix fx - | FCoFix(cfx,e) when is_subs_id e & is_lift_id lfts -> mkCoFix cfx + | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> mkFix fx + | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> mkCoFix cfx | _ -> to_constr term_of_fconstr_lift lfts v in term_of_fconstr_lift el_id diff --git a/kernel/constr.ml b/kernel/constr.ml index 8b7505aeb..f751343bc 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -106,7 +106,7 @@ let rels = [|Rel 1;Rel 2;Rel 3;Rel 4;Rel 5;Rel 6;Rel 7; Rel 8; Rel 9;Rel 10;Rel 11;Rel 12;Rel 13;Rel 14;Rel 15; Rel 16|] -let mkRel n = if 0<n & n<=16 then rels.(n-1) else Rel n +let mkRel n = if 0<n && n<=16 then rels.(n-1) else Rel n (* Construct a type *) let mkProp = Sort Sorts.prop @@ -346,7 +346,7 @@ let compare_head f t1 t2 = | Ind c1, Ind c2 -> eq_ind c1 c2 | Construct c1, Construct c2 -> eq_constructor c1 c2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - f p1 p2 & f c1 c2 && Array.equal f bl1 bl2 + f p1 p2 && f c1 c2 && Array.equal f bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2 @@ -463,19 +463,19 @@ let hasheq t1 t2 = | Meta m1, Meta m2 -> m1 == m2 | Var id1, Var id2 -> id1 == id2 | Sort s1, Sort s2 -> s1 == s2 - | Cast (c1,k1,t1), Cast (c2,k2,t2) -> c1 == c2 & k1 == k2 & t1 == t2 - | Prod (n1,t1,c1), Prod (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 - | Lambda (n1,t1,c1), Lambda (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 + | Cast (c1,k1,t1), Cast (c2,k2,t2) -> c1 == c2 && k1 == k2 && t1 == t2 + | Prod (n1,t1,c1), Prod (n2,t2,c2) -> n1 == n2 && t1 == t2 && c1 == c2 + | Lambda (n1,t1,c1), Lambda (n2,t2,c2) -> n1 == n2 && t1 == t2 && c1 == c2 | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) -> - n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2 - | App (c1,l1), App (c2,l2) -> c1 == c2 & array_eqeq l1 l2 - | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 & array_eqeq l1 l2 + n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2 + | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && array_eqeq l1 l2 | Const c1, Const c2 -> c1 == c2 | Ind (sp1,i1), Ind (sp2,i2) -> sp1 == sp2 && Int.equal i1 i2 | Construct ((sp1,i1),j1), Construct ((sp2,i2),j2) -> sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2 | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) -> - ci1 == ci2 & p1 == p2 & c1 == c2 & array_eqeq bl1 bl2 + ci1 == ci2 && p1 == p2 && c1 == c2 && array_eqeq bl1 bl2 | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) -> Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 @@ -484,9 +484,9 @@ let hasheq t1 t2 = && array_eqeq bl1 bl2 | CoFix(ln1,(lna1,tl1,bl1)), CoFix(ln2,(lna2,tl2,bl2)) -> Int.equal ln1 ln2 - & array_eqeq lna1 lna2 - & array_eqeq tl1 tl2 - & array_eqeq bl1 bl2 + && array_eqeq lna1 lna2 + && array_eqeq tl1 tl2 + && array_eqeq bl1 bl2 | _ -> false (** Note that the following Make has the side effect of creating diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 319f95c61..998bba492 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -49,7 +49,7 @@ let rec reloc_rel n = function let rec is_lift_id = function | ELID -> true - | ELSHFT(e,n) -> Int.equal n 0 & is_lift_id e + | ELSHFT(e,n) -> Int.equal n 0 && is_lift_id e | ELLFT (_,e) -> is_lift_id e (*********************) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 9a11e47dc..9d2580ce4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -282,7 +282,7 @@ let typecheck_inductive env mie = | _ -> true end -> (* Predicative set: check that the content is indeed predicative *) - if not (is_type0m_univ lev) & not (is_type0_univ lev) then + if not (is_type0m_univ lev) && not (is_type0_univ lev) then raise (InductiveError LargeNonPropInductiveNotInType); Inl (info,full_arity,s), cst | Prop _ -> diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 1c9780669..d52877fd2 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -659,7 +659,7 @@ let check_one_fix renv recpos def = match kind_of_term f with | Rel p -> (* Test if [p] is a fixpoint (recursive call) *) - if renv.rel_min <= p & p < renv.rel_min+nfi then + if renv.rel_min <= p && p < renv.rel_min+nfi then begin List.iter (check_rec_call renv []) l; (* the position of the invoked fixpoint: *) diff --git a/kernel/term.ml b/kernel/term.ml index 258f8423c..fa204b570 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -198,7 +198,7 @@ let is_small = function | Prop _ -> true | _ -> false -let iskind c = isprop c or is_Type c +let iskind c = isprop c || is_Type c (* Tests if an evar *) let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false diff --git a/kernel/vars.ml b/kernel/vars.ml index 12c1529c8..c7ec69c87 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -62,7 +62,7 @@ let isMeta c = match Constr.kind c with let noccur_with_meta n m term = let rec occur_rec n c = match Constr.kind c with - | Constr.Rel p -> if n<=p & p<n+m then raise LocalOccur + | Constr.Rel p -> if n<=p && p<n+m then raise LocalOccur | Constr.App(f,cl) -> (match Constr.kind f with | Constr.Cast (c,_,_) when isMeta c -> () diff --git a/lib/bigint.ml b/lib/bigint.ml index be207f667..231dc178f 100644 --- a/lib/bigint.ml +++ b/lib/bigint.ml @@ -92,7 +92,7 @@ let normalize_pos n = let normalize_neg n = let k = ref 1 in - while !k < Array.length n & n.(!k) = base - 1 do incr k done; + 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 Int.equal (Array.length n') 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n') @@ -132,10 +132,10 @@ let neg m = let push_carry r j = let j = ref j in - while !j > 0 & r.(!j) < 0 do + while !j > 0 && r.(!j) < 0 do r.(!j) <- r.(!j) + base; decr j; r.(!j) <- r.(!j) - 1 done; - while !j > 0 & r.(!j) >= base do + while !j > 0 && r.(!j) >= base do r.(!j) <- r.(!j) - base; decr j; r.(!j) <- r.(!j) + 1 done; (* here r.(0) could be in [-2*base;2*base-1] *) @@ -173,9 +173,9 @@ let sub n m = else let r = neg m in add_to r n (Array.length r - Array.length n) let mult m n = - if m = zero or n = zero then zero else + if m = zero || n = zero then zero else let l = Array.length m + Array.length n in - let r = Array.create l 0 in + let r = Array.make l 0 in for i = Array.length m - 1 downto 0 do for j = Array.length n - 1 downto 0 do let p = m.(i) * n.(j) + r.(i+j+1) in @@ -193,22 +193,22 @@ let mult m n = let is_strictly_neg n = n<>[||] && n.(0) < 0 let is_strictly_pos n = n<>[||] && n.(0) > 0 -let is_neg_or_zero n = n=[||] or n.(0) < 0 -let is_pos_or_zero n = n=[||] or n.(0) > 0 +let is_neg_or_zero n = n=[||] || n.(0) < 0 +let is_pos_or_zero n = n=[||] || n.(0) > 0 (* Is m without its i first blocs less then n without its j first blocs ? Invariant : |m|-i = |n|-j *) let rec less_than_same_size m n i j = i < Array.length m && - (m.(i) < n.(j) or (m.(i) = n.(j) && less_than_same_size m n (i+1) (j+1))) + (m.(i) < n.(j) || (m.(i) = n.(j) && less_than_same_size m n (i+1) (j+1))) let less_than m n = if is_strictly_neg m then - is_pos_or_zero n or Array.length m > Array.length n - or (Array.length m = Array.length n && less_than_same_size m n 0 0) + is_pos_or_zero n || Array.length m > Array.length n + || (Array.length m = Array.length n && less_than_same_size m n 0 0) else - is_strictly_pos n && (Array.length m < Array.length n or + is_strictly_pos n && (Array.length m < Array.length n || (Array.length m = Array.length n && less_than_same_size m n 0 0)) (* For this equality test it is critical that n and m are canonical *) @@ -219,11 +219,11 @@ let equal m n = (m = n) let less_than_shift_pos k m n = (Array.length m - k < Array.length n) - or (Array.length m - k = Array.length n && less_than_same_size m n k 0) + || (Array.length m - k = Array.length n && less_than_same_size m n k 0) let rec can_divide k m d i = - (i = Array.length d) or - (m.(k+i) > d.(i)) or + (i = Array.length d) || + (m.(k+i) > d.(i)) || (m.(k+i) = d.(i) && can_divide k m d (i+1)) (* For two big nums m and d and a small number q, @@ -258,7 +258,7 @@ let euclid m d = let q,r = if less_than m d then (zero,m) else let ql = Array.length m - Array.length d in - let q = Array.create (ql+1) 0 in + let q = Array.make (ql+1) 0 in let i = ref 0 in while not (less_than_shift_pos !i m d) do if Int.equal m.(!i) 0 then incr i else @@ -288,7 +288,7 @@ let euclid m d = let of_string s = let len = String.length s in - let isneg = len > 1 & s.[0] = '-' in + let isneg = len > 1 && s.[0] = '-' in let d = ref (if isneg then 1 else 0) in while !d < len && s.[!d] = '0' do incr d done; if !d = len then zero else @@ -296,7 +296,7 @@ let of_string s = let h = String.sub s (!d) r in let e = if h<>"" then 1 else 0 in let l = (len - !d) / size in - let a = Array.create (l + e) 0 in + let a = Array.make (l + e) 0 in 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) @@ -384,28 +384,28 @@ let app_pair f (m, n) = (f m, f n) let add m n = - if Obj.is_int m & Obj.is_int n + if Obj.is_int m && Obj.is_int n then of_int (coerce_to_int m + coerce_to_int n) else of_ints (add (to_ints m) (to_ints n)) let sub m n = - if Obj.is_int m & Obj.is_int n + if Obj.is_int m && Obj.is_int n then of_int (coerce_to_int m - coerce_to_int n) else of_ints (sub (to_ints m) (to_ints n)) let mult m n = - if Obj.is_int m & Obj.is_int n + if Obj.is_int m && Obj.is_int n then of_int (coerce_to_int m * coerce_to_int n) else of_ints (mult (to_ints m) (to_ints n)) let euclid m n = - if Obj.is_int m & Obj.is_int n + if Obj.is_int m && Obj.is_int n then app_pair of_int (coerce_to_int m / coerce_to_int n, coerce_to_int m mod coerce_to_int n) else app_pair of_ints (euclid (to_ints m) (to_ints n)) let less_than m n = - if Obj.is_int m & Obj.is_int n + if Obj.is_int m && Obj.is_int n then coerce_to_int m < coerce_to_int n else less_than (to_ints m) (to_ints n) diff --git a/lib/cArray.ml b/lib/cArray.ml index eff317aac..f81baef45 100644 --- a/lib/cArray.ml +++ b/lib/cArray.ml @@ -301,7 +301,7 @@ let map2 f v1 v2 = if Int.equal (Array.length v1) 0 then [| |] else begin - let res = Array.create (Array.length v1) (f v1.(0) v2.(0)) in + let res = Array.make (Array.length v1) (f v1.(0) v2.(0)) in for i = 1 to pred (Array.length v1) do res.(i) <- f v1.(i) v2.(i) done; @@ -314,7 +314,7 @@ let map2_i f v1 v2 = if Int.equal (Array.length v1) 0 then [| |] else begin - let res = Array.create (Array.length v1) (f 0 v1.(0) v2.(0)) in + let res = Array.make (Array.length v1) (f 0 v1.(0) v2.(0)) in for i = 1 to pred (Array.length v1) do res.(i) <- f i v1.(i) v2.(i) done; @@ -327,7 +327,7 @@ let map3 f v1 v2 v3 = 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 + let res = Array.make (Array.length v1) (f v1.(0) v2.(0) v3.(0)) in for i = 1 to pred (Array.length v1) do res.(i) <- f v1.(i) v2.(i) v3.(i) done; @@ -337,7 +337,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 Int.equal l 0 then [||] else begin - let r = Array.create l (f a.(0)) in + let r = Array.make l (f a.(0)) in for i = 1 to l - 1 do r.(i) <- f a.(i) done; diff --git a/lib/cString.ml b/lib/cString.ml index 1cb153b66..823a35679 100644 --- a/lib/cString.ml +++ b/lib/cString.ml @@ -107,7 +107,7 @@ let map f s = let drop_simple_quotes s = let n = String.length s in - if n > 2 && s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s + if n > 2 && s.[0] = '\'' && s.[n-1] = '\'' then String.sub s 1 (n-2) else s (* substring searching... *) diff --git a/lib/hashcons.ml b/lib/hashcons.ml index 9a5f20f0c..33f2c578f 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -151,10 +151,10 @@ exception NotEq (* From CAMLLIB/caml/mlvalues.h *) let no_scan_tag = 251 -let tuple_p obj = Obj.is_block obj & (Obj.tag obj < no_scan_tag) +let tuple_p obj = Obj.is_block obj && (Obj.tag obj < no_scan_tag) let comp_obj o1 o2 = - if tuple_p o1 & tuple_p o2 then + if tuple_p o1 && tuple_p o2 then let n1 = Obj.size o1 and n2 = Obj.size o2 in if n1=n2 then try diff --git a/lib/hashset.ml b/lib/hashset.ml index 6f62e1a90..279beb1c9 100644 --- a/lib/hashset.ml +++ b/lib/hashset.ml @@ -51,8 +51,8 @@ module Make (E : EqType) = let sz = if sz < 7 then 7 else sz in let sz = if sz > Sys.max_array_length then Sys.max_array_length else sz in { - table = Array.create sz emptybucket; - hashes = Array.create sz [| |]; + table = Array.make sz emptybucket; + hashes = Array.make sz [| |]; limit = limit; oversize = 0; rover = 0; diff --git a/lib/predicate.ml b/lib/predicate.ml index e419aa6e9..a60b3dadd 100644 --- a/lib/predicate.ml +++ b/lib/predicate.ml @@ -54,8 +54,8 @@ module Make(Ord: OrderedType) = let full = (true,EltSet.empty) (* assumes the set is infinite *) - let is_empty (b,s) = not b & EltSet.is_empty s - let is_full (b,s) = b & EltSet.is_empty s + let is_empty (b,s) = not b && EltSet.is_empty s + let is_full (b,s) = b && EltSet.is_empty s let mem x (b,s) = if b then not (EltSet.mem x s) else EltSet.mem x s @@ -92,6 +92,6 @@ module Make(Ord: OrderedType) = | ((true,_),(false,_)) -> false let equal (b1,s1) (b2,s2) = - b1=b2 & EltSet.equal s1 s2 + b1=b2 && EltSet.equal s1 s2 end diff --git a/lib/profile.ml b/lib/profile.ml index 6f878d2f6..6a1b45a39 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -279,7 +279,7 @@ let format_profile (table, outside, total) = Printf.printf "%-23s %9s %9s %10s %10s %10s\n" "Function name" "Own time" "Tot. time" "Own alloc" "Tot. alloc" "Calls "; - let l = Sort.list (fun (_,{tottime=p}) (_,{tottime=p'}) -> p > p') table in + let l = List.sort (fun (_,{tottime=p}) (_,{tottime=p'}) -> p' - p) table in List.iter (fun (name,e) -> Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f %6d %6d\n" @@ -352,7 +352,7 @@ let close_profile print = let print_profile () = close_profile true let declare_profile name = - if name = "___outside___" or name = "___total___" then + if name = "___outside___" || name = "___total___" then failwith ("Error: "^name^" is a reserved keyword"); let e = create_record () in prof_table := (name,e)::!prof_table; diff --git a/lib/unicode.ml b/lib/unicode.ml index febf805ae..f26af1014 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -19,7 +19,7 @@ exception Unsupported trade-off between speed and space after some benchmarks.) *) (* A 256ko table, initially filled with zeros. *) -let table = Array.create (1 lsl 17) 0 +let table = Array.make (1 lsl 17) 0 (* Associate a 2-bit pattern to each status at position [i]. Only the 3 lowest bits of [i] are taken into account to @@ -150,7 +150,7 @@ let next_utf8 s i = if l = 0 then raise End_of_input else let a = Char.code s.[i] in if a <= 0x7F then 1, a - else if a land 0x40 = 0 or l = 1 then err () + else if a land 0x40 = 0 || l = 1 then err () else let b = Char.code s.[i+1] in if b land 0xC0 <> 0x80 then err () else if a land 0x20 = 0 then 2, (a land 0x1F) lsl 6 + (b land 0x3F) diff --git a/lib/util.ml b/lib/util.ml index 2db11131d..2358ba48f 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -26,10 +26,10 @@ let pi3 (_,_,a) = a (* Characters *) -let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z') +let is_letter c = (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') let is_digit c = (c >= '0' && c <= '9') let is_ident_tail c = - is_letter c or is_digit c || c = '\'' or c = '_' + is_letter c || is_digit c || c = '\'' || c = '_' let is_blank = function | ' ' | '\r' | '\t' | '\n' -> true | _ -> false @@ -48,7 +48,7 @@ let subst_command_placeholder s t = let buff = Buffer.create (String.length s + String.length t) in let i = ref 0 in while (!i < String.length s) do - if s.[!i] = '%' & !i+1 < String.length s & s.[!i+1] = 's' + if s.[!i] = '%' && !i+1 < String.length s && s.[!i+1] = 's' then (Buffer.add_string buff t;incr i) else Buffer.add_char buff s.[!i]; incr i diff --git a/library/declare.ml b/library/declare.ml index 96bbf07d5..475bc098a 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -120,7 +120,7 @@ let open_constant i ((sp,kn), obj) = Nametab.push (Nametab.Exactly i) sp (ConstRef con) let exists_name id = - variable_exists id or Global.exists_objlabel (Label.of_id id) + variable_exists id || Global.exists_objlabel (Label.of_id id) let check_exists sp = let id = basename sp in diff --git a/library/goptions.ml b/library/goptions.ml index 4151e6774..6e2c6ae72 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -211,7 +211,7 @@ let check_key key = try error "Sorry, this option name is already used." with Not_found -> if List.mem_assoc (nickname key) !string_table - or List.mem_assoc (nickname key) !ref_table + || List.mem_assoc (nickname key) !ref_table then error "Sorry, this option name is already used." open Libobject diff --git a/library/heads.ml b/library/heads.ml index 2a42888d5..c52a5eb23 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -109,7 +109,7 @@ let kind_of_head env t = (* enough arguments to [cst] *) k,List.skipn n l,List.nth l (i-1) in let l' = List.make q (mkMeta 0) @ rest in - aux k' l' a (with_subcase or with_case) + aux k' l' a (with_subcase || with_case) | ConstructorHead when with_case -> NotImmediatelyComputableHead | x -> x in aux 0 [] t false diff --git a/library/impargs.ml b/library/impargs.ml index 0026bc489..66900ee42 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -174,8 +174,8 @@ let is_flexible_reference env bound depth f = let push_lift d (e,n) = (push_rel d e,n+1) let is_reversible_pattern bound depth f l = - isRel f & let n = destRel f in (n < bound+depth) & (n >= depth) & - Array.for_all (fun c -> isRel c & destRel c < depth) l & + isRel f && let n = destRel f in (n < bound+depth) && (n >= depth) && + Array.for_all (fun c -> isRel c && destRel c < depth) l && Array.distinct l (* Precondition: rels in env are for inductive types only *) @@ -184,13 +184,13 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc = let hd = if strict then whd_betadeltaiota env c else c in let c = if strongly_strict then hd else c in match kind_of_term hd with - | Rel n when (n < bound+depth) & (n >= depth) -> + | Rel n when (n < bound+depth) && (n >= depth) -> let i = bound + depth - n - 1 in acc.(i) <- update pos rig acc.(i) - | App (f,l) when revpat & is_reversible_pattern bound depth f l -> + | App (f,l) when revpat && is_reversible_pattern bound depth f l -> let i = bound + depth - destRel f - 1 in acc.(i) <- update pos rig acc.(i) - | App (f,_) when rig & is_flexible_reference env bound depth f -> + | App (f,_) when rig && is_flexible_reference env bound depth f -> if strict then () else iter_constr_with_full_binders push_lift (frec false) ed c | Case _ when rig -> @@ -246,7 +246,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = let compute_implicits_flags env f all t = compute_implicits_gen - (f.strict or f.strongly_strict) f.strongly_strict + (f.strict || f.strongly_strict) f.strongly_strict f.reversible_pattern f.contextual all env t let compute_auto_implicits env flags enriching t = @@ -289,9 +289,9 @@ let force_inference_of = function (* [in_ctx] means we know the expected type, [n] is the index of the argument *) let is_inferable_implicit in_ctx n = function | None -> false - | Some (_,DepRigid (Hyp p),_) -> in_ctx or n >= p + | Some (_,DepRigid (Hyp p),_) -> in_ctx || n >= p | Some (_,DepFlex (Hyp p),_) -> false - | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx or n >= q + | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx || n >= q | Some (_,DepRigid Conclusion,_) -> in_ctx | Some (_,DepFlex Conclusion,_) -> false | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx @@ -328,7 +328,7 @@ let check_correct_manual_implicits autoimps l = if not forced then error ("Wrong or non-dependent implicit argument name: "^(Id.to_string id)^".") | ExplByPos (i,_id),_t -> - if i<1 or i>List.length autoimps then + if i<1 || i>List.length autoimps then error ("Bad implicit argument number: "^(string_of_int i)^".") else errorlabstrm "" @@ -663,7 +663,7 @@ let declare_manual_implicits local ref ?enriching l = | _ -> check_rigidity isrigid; let l = List.map (fun imps -> (imps,List.length imps)) l in - let l = Sort.list (fun (_,n1) (_,n2) -> n1 > n2) l in + let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in check_inclusion l; let nargs = List.length autoimpls in List.map (fun (imps,n) -> diff --git a/library/library.ml b/library/library.ml index 44e8286ce..2a495f0cf 100644 --- a/library/library.ml +++ b/library/library.ml @@ -144,7 +144,7 @@ let open_library export explicit_libs m = (* Only libraries indirectly to open are not reopen *) (* Libraries explicitly mentionned by the user are always reopen *) List.exists (eq_lib_name m) explicit_libs - or not (library_is_opened m.library_name) + || not (library_is_opened m.library_name) then begin register_open_library export m; Declaremods.really_import_module (MPfile m.library_name) diff --git a/library/nameops.ml b/library/nameops.ml index 22a21a4d5..a62d55dfc 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -58,7 +58,7 @@ let make_ident sa = function | Some n -> let c = Char.code (String.get sa (String.length sa -1)) in let s = - if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n) + if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n) else sa ^ "_" ^ (string_of_int n) in Id.of_string s | None -> Id.of_string (String.copy sa) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 4173270c1..b476f5303 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -138,7 +138,7 @@ let check_utf8_trailing_byte cs c = (* but don't certify full utf8 compliance (e.g. no emptyness check) *) let lookup_utf8_tail c cs = let c1 = Char.code c in - if Int.equal (c1 land 0x40) 0 or Int.equal (c1 land 0x38) 0x38 then error_utf8 cs + if Int.equal (c1 land 0x40) 0 || Int.equal (c1 land 0x38) 0x38 then error_utf8 cs else let n, unicode = if Int.equal (c1 land 0x20) 0 then diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 0903f85a0..4ad681c05 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1248,7 +1248,7 @@ let rec non_stricts add cand = function let n = List.length i in let cand = lift n cand in let cand = pop n (non_stricts add cand t) in - Sort.merge (<=) cand c) [] v + List.merge Pervasives.compare cand c) [] v (* [merge] may duplicates some indices, but I don't mind. *) | MLmagic t -> non_stricts add cand t diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 02503ab47..3dd384ee8 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -271,7 +271,7 @@ let fourier_lineq lineq1 = f.hflin.fhom) lineq1; let sys= List.map (fun h-> - let v=Array.create ((!nvar)+1) r0 in + let v=Array.make ((!nvar)+1) r0 in Constrhash.iter (fun x c -> v.(Constrhash.find hvar x)<-c) h.hflin.fhom; ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict)) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 15e284398..356853573 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -916,9 +916,9 @@ let generalize_non_dep hyp g = let to_revert,_ = Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> if List.mem hyp hyps - or List.exists (Termops.occur_var_in_decl env hyp) keep - or Termops.occur_var env hyp hyp_typ - or Termops.is_section_variable hyp (* should be dangerous *) + || List.exists (Termops.occur_var_in_decl env hyp) keep + || Termops.occur_var env hyp hyp_typ + || Termops.is_section_variable hyp (* should be dangerous *) then (clear,decl::keep) else (hyp::clear,keep)) ~init:([],[]) (pf_env g) diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index 339e10661..f993dc14f 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -218,7 +218,7 @@ struct let fold = P.fold - let is_null p = fold (fun mn vl b -> b & sign_num vl = 0) p true + let is_null p = fold (fun mn vl b -> b && sign_num vl = 0) p true let compare = compare compare_num diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index 5ad546588..6beb96c38 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -133,7 +133,7 @@ let deg m = m.(0) let mult_mon m m' = let d = nvar m in - let m'' = Array.create (d+1) 0 in + let m'' = Array.make (d+1) 0 in for i=0 to d do m''.(i)<- (m.(i)+m'.(i)); done; @@ -167,7 +167,7 @@ let compare_mon m m' = let div_mon m m' = let d = nvar m in - let m'' = Array.create (d+1) 0 in + let m'' = Array.make (d+1) 0 in for i=0 to d do m''.(i)<- (m.(i)-m'.(i)); done; @@ -198,7 +198,7 @@ let set_deg m = (* lcm *) let ppcm_mon m m' = let d = nvar m in - let m'' = Array.create (d+1) 0 in + let m'' = Array.make (d+1) 0 in for i=1 to d do m''.(i)<- (max m.(i) m'.(i)); done; @@ -397,7 +397,7 @@ let zeroP = [] (* returns a constant polynom ial with d variables *) let polconst d c = - let m = Array.create (d+1) 0 in + let m = Array.make (d+1) 0 in let m = set_deg m in [(c,m)] @@ -430,7 +430,7 @@ let coef_of_int x = P.of_num (Num.Int x) (* variable i *) let gen d i = - let m = Array.create (d+1) 0 in + let m = Array.make (d+1) 0 in m.(i) <- 1; let m = set_deg m in [((coef_of_int 1),m)] @@ -464,7 +464,7 @@ let puisP p n= let d = nvar (snd (List.hd p)) in let rec puisP n = match n with - 0 -> [coef1, Array.create (d+1) 0] + 0 -> [coef1, Array.make (d+1) 0] | 1 -> p |_ -> multP p (puisP (n-1)) in puisP n @@ -503,13 +503,13 @@ let lm p = snd (List.hd (ppol p)) let nallpol = ref 0 -let allpol = ref (Array.create 1000 polynom0) +let allpol = ref (Array.make 1000 polynom0) let new_allpol p s = nallpol := !nallpol + 1; if !nallpol >= Array.length !allpol then - allpol := Array.append !allpol (Array.create !nallpol polynom0); + allpol := Array.append !allpol (Array.make !nallpol polynom0); let p = {pol = ref p; num = !nallpol; sugar = s} in !allpol.(!nallpol)<- p; p @@ -1028,7 +1028,7 @@ let in_ideal d lp p = Hashtbl.clear hmon; Hashtbl.clear coefpoldep; nallpol := 0; - allpol := Array.create 1000 polynom0; + allpol := Array.make 1000 polynom0; homogeneous := List.for_all is_homogeneous (p::lp); if !homogeneous then info "homogeneous polynomials\n"; info ("p: "^(stringPcut p)^"\n"); diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml index 638242462..8e2fc07c0 100644 --- a/plugins/nsatz/utile.ml +++ b/plugins/nsatz/utile.ml @@ -81,7 +81,7 @@ let facteurs_liste div constant lp = c est un élément quelconque de E. *) let factorise_tableau div zero c f l1 = - let res = Array.create (Array.length f) (c,[]) in + let res = Array.make (Array.length f) (c,[]) in Array.iteri (fun i p -> let r = ref p in let li = ref [] in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index f98aba0a8..0dd137b6f 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1254,7 +1254,7 @@ let replay_history tactic_normalisation = and id2 = hyp_of_tag e2.id in let eq1 = val_of(decompile e1) and eq2 = val_of(decompile e2) in - if k1 =? one & e2.kind = EQUA then + if k1 =? one && e2.kind = EQUA then let tac_thm = match e1.kind with | EQUA -> Lazy.force coq_OMEGA5 diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index 800254671..60887b451 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -36,9 +36,9 @@ module MakeOmegaSolver (Int:INT) = struct type bigint = Int.bigint let (<?) = Int.less_than -let (<=?) x y = Int.less_than x y or x = y +let (<=?) x y = Int.less_than x y || x = y let (>?) x y = Int.less_than y x -let (>=?) x y = Int.less_than y x or x = y +let (>=?) x y = Int.less_than y x || x = y let (=?) = (=) let (+) = Int.add let (-) = Int.sub @@ -239,7 +239,7 @@ let add_event, history, clear_history = (fun () -> !accu), (fun () -> accu := []) -let nf_linear = Sort.list (fun x y -> x.v > y.v) +let nf_linear = List.sort (fun x y -> Pervasives.(-) y.v x.v) let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x)) @@ -301,16 +301,16 @@ let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) = end end else let gcd = pgcd_l (List.map (fun f -> abs f.c) e) in - if eq_flag=EQUA & x mod gcd <> zero then begin + if eq_flag=EQUA && x mod gcd <> zero then begin add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE - end else if eq_flag=DISE & x mod gcd <> zero then begin + end else if eq_flag=DISE && x mod gcd <> zero then begin add_event (FORGET_C eq.id); [] end else if gcd <> one then begin let c = floor_div x gcd in let d = x - c * gcd in let new_eq = {id=id; kind=eq_flag; constant=c; body=map_eq_linear (fun c -> c / gcd) e} in - add_event (if eq_flag=EQUA or eq_flag = DISE then EXACT_DIVIDE(eq,gcd) + add_event (if eq_flag=EQUA || eq_flag = DISE then EXACT_DIVIDE(eq,gcd) else DIVIDE_AND_APPROX(eq,new_eq,gcd,d)); [new_eq] end else [eq] @@ -472,7 +472,7 @@ let select_variable system = Hashtbl.iter (fun v ({contents = c}) -> incr var_cpt; - if c <? !cmin or !vmin = (-1) then begin vmin := v; cmin := c end) + if c <? !cmin || !vmin = (-1) then begin vmin := v; cmin := c end) table; if !var_cpt < 1 then raise SOLVED_SYSTEM; !vmin diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 998e54767..c09e2d743 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -245,7 +245,7 @@ let compute_ivs gl f cs = (* Then we test if the RHS is the RHS for variables *) else begin match decompose_app bodyi with | vmf, [_; _; a3; a4 ] - when isRel a3 & isRel a4 & + when isRel a3 && isRel a4 && pf_conv_x gl vmf (Lazy.force coq_varmap_find)-> v_lhs := Some (compute_lhs @@ -260,7 +260,7 @@ let compute_ivs gl f cs = end) lci; - if !c_lhs = None & !v_lhs = None then i_can't_do_that (); + if !c_lhs = None && !v_lhs = None then i_can't_do_that (); (* The Cases predicate is a lambda; we assume no dependency *) let p = match kind_of_term p with @@ -295,7 +295,7 @@ binary search trees (see file \texttt{Quote.v}) *) and variables (open terms) *) let rec closed_under cset t = - (ConstrSet.mem t cset) or + (ConstrSet.mem t cset) || (match (kind_of_term t) with | Cast(c,_,_) -> closed_under cset c | App(f,l) -> closed_under cset f && Array.for_all (closed_under cset) l @@ -357,7 +357,7 @@ let path_of_int n = (* This function does not descend under binders (lambda and Cases) *) let rec subterm gl (t : constr) (t' : constr) = - (pf_conv_x gl t t') or + (pf_conv_x gl t t') || (match (kind_of_term t) with | App (f,args) -> Array.exists (fun t -> subterm gl t t') args | Cast(t,_,_) -> (subterm gl t t') diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 75fe49bcf..af833dacb 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -352,7 +352,7 @@ let parse_rel gl t = let is_scalar t = let rec aux t = match destructurate t with - | Kapp(("Z.add"|"Z.sub"|"Z.mul"),[t1;t2]) -> aux t1 & aux t2 + | Kapp(("Z.add"|"Z.sub"|"Z.mul"),[t1;t2]) -> aux t1 && aux t2 | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true | _ -> false in diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index b6fdf315c..180d15009 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -45,7 +45,7 @@ let interp_ascii_string dloc s = let p = if String.length s = 1 then int_of_char s.[0] else - if String.length s = 3 & is_digit s.[0] & is_digit s.[1] & is_digit s.[2] + if String.length s = 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] then int_of_string s else user_err_loc (dloc,"interp_ascii_string", diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index bddca9e65..efbd140ee 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -72,19 +72,19 @@ let bignat_of_r = let rec bignat_of_pos = function (* 1+1 *) | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)]) - when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two + when p = glob_Rplus && o1 = glob_R1 && o2 = glob_R1 -> two (* 1+(1+1) *) | GApp (_,GRef (_,p1), [GRef (_,o1); GApp(_,GRef (_,p2),[GRef(_,o2);GRef(_,o3)])]) - when p1 = glob_Rplus & p2 = glob_Rplus & - o1 = glob_R1 & o2 = glob_R1 & o3 = glob_R1 -> three + when p1 = glob_Rplus && p2 = glob_Rplus && + o1 = glob_R1 && o2 = glob_R1 && o3 = glob_R1 -> three (* (1+1)*b *) | GApp (_,GRef (_,p), [a; b]) when p = glob_Rmult -> if bignat_of_pos a <> two then raise Non_closed_number; mult_2 (bignat_of_pos b) (* 1+(1+1)*b *) | GApp (_,GRef (_,p1), [GRef (_,o); GApp (_,GRef (_,p2),[a;b])]) - when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1 -> + when p1 = glob_Rplus && p2 = glob_Rmult && o = glob_R1 -> if bignat_of_pos a <> two then raise Non_closed_number; add_1 (mult_2 (bignat_of_pos b)) | _ -> raise Non_closed_number 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 diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 0f6a5e893..0e0480836 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -126,7 +126,7 @@ let need_expansion impl ref = let typ = Global.type_of_global ref in let ctx = prod_assum typ in let nprods = List.length (List.filter (fun (_,b,_) -> Option.is_empty b) ctx) in - not (List.is_empty impl) && List.length impl >= nprods & + not (List.is_empty impl) && List.length impl >= nprods && let _,lastimpl = List.chop nprods impl in List.exists is_status_implicit lastimpl diff --git a/printing/printer.ml b/printing/printer.ml index 19dd81dcd..0e5d6721e 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -778,7 +778,7 @@ let print_record env mind mib = pr_univ_cstr mib.mind_constraints) let pr_mutual_inductive_body env mind mib = - if mib.mind_record & not !Flags.raw_print then + if mib.mind_record && not !Flags.raw_print then print_record env mind mib else print_mutual_inductive env mind mib diff --git a/proofs/logic.ml b/proofs/logic.ml index 84bbd9751..e93319cae 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -333,7 +333,7 @@ let check_meta_variables c = raise (RefinerError (NonLinearProof c)) let check_conv_leq_goal env sigma arg ty conclty = - if !check & not (is_conv_leq env sigma ty conclty) then + if !check && not (is_conv_leq env sigma ty conclty) then raise (RefinerError (BadType (arg,ty,conclty))) let goal_type_of env sigma c = @@ -371,7 +371,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let (acc',hdty,sigma,applicand) = 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)) -> (* Sort-polymorphism of definition and inductive types *) goalacc, type_of_global_reference_knowing_conclusion env sigma f conclty, @@ -423,8 +423,8 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if isInd f or isConst f - & not (Array.exists occur_meta l) (* we could be finer *) + if isInd f || isConst f + && not (Array.exists occur_meta l) (* we could be finer *) then (goalacc,type_of_global_reference_knowing_parameters env sigma f l,sigma,f) else mk_hdgoals sigma goal goalacc f diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index d73561f37..1b49f9ff8 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -71,7 +71,7 @@ let rec drop_spaces inst i = else i let possibly_unquote s = - if String.length s >= 2 & s.[0] == '"' & s.[String.length s - 1] == '"' then + if String.length s >= 2 && s.[0] == '"' && s.[String.length s - 1] == '"' then String.sub s 1 (String.length s - 2) else s diff --git a/tactics/auto.ml b/tactics/auto.ml index d743135a2..6ed05d6b3 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -148,7 +148,7 @@ let rebuild_dn st ((l,l',dn) : search_entry) = let lookup_tacs (hdc,c) st (l,l',dn) = let l' = List.map snd (Bounded_net.lookup st dn c) in let sl' = List.stable_sort pri_order_int l' in - Sort.merge pri_order l sl' + List.merge pri_order_int l sl' module Constr_map = Map.Make(RefOrdered) @@ -334,16 +334,16 @@ module Hint_db = struct with Not_found -> empty_se let map_none db = - List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat) []) + List.map snd (List.merge pri_order_int (List.map snd db.hintdb_nopat) []) let map_all k db = let (l,l',_) = find k db in - List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l') + List.map snd (List.merge pri_order_int (List.map snd db.hintdb_nopat @ l) l') let map_auto (k,c) db = let st = if db.use_dn then Some db.hintdb_state else None in let l' = lookup_tacs (k,c) st (find k db) in - List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat) l') + List.map snd (List.merge pri_order_int (List.map snd db.hintdb_nopat) l') let is_exact = function | Give_exact _ -> true diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 14a9ae9c2..d6e51a15d 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -65,7 +65,7 @@ let contradiction_context gl = let is_negation_of env sigma typ t = match kind_of_term (whd_betadeltaiota env sigma t) with - | Prod (na,t,u) -> is_empty_type u & is_conv_leq env sigma typ t + | Prod (na,t,u) -> is_empty_type u && is_conv_leq env sigma typ t | _ -> false let contradiction_term (c,lbind as cl) gl = diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 49b7ec710..1756f89ce 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -32,7 +32,7 @@ open Locusops let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state } let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in - if occur_existential t1 or occur_existential t2 then + if occur_existential t1 || occur_existential t2 then tclTHEN (Clenvtac.unify ~flags t1) (exact_check c) gl else exact_check c gl diff --git a/tactics/equality.ml b/tactics/equality.ml index d1d4e003d..04d6b9d8e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -480,7 +480,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl = in let t1 = pf_apply get_type_of gl c1 and t2 = pf_apply get_type_of gl c2 in - if unsafe or (pf_conv_x gl t1 t2) then + if unsafe || (pf_conv_x gl t1 t2) then let e = build_coq_eq () in let sym = build_coq_eq_sym () in let eq = applist (e, [t1;c1;c2]) in @@ -1060,7 +1060,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let make_iterated_tuple env sigma dflt (z,zty) = let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in let sort_of_zty = get_sort_of env sigma zty in - let sorted_rels = Sort.list (<) (Int.Set.elements rels) in + let sorted_rels = List.sort Pervasives.compare (Int.Set.elements rels) in let (tuple,tuplety) = List.fold_left (make_tuple env sigma) (z,zty) sorted_rels in @@ -1208,7 +1208,7 @@ let postInjEqTac ipats c n = let injEq ipats = let l2r = - if use_injection_pattern_l2r_order () & ipats <> None then true else false + if use_injection_pattern_l2r_order () && ipats <> None then true else false in injEqThen (postInjEqTac ipats) l2r diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index d870bfa1d..534b90491 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -91,7 +91,7 @@ let match_with_one_constructor style onlybinary allow_rec t = | Ind ind -> let (mib,mip) = Global.lookup_inductive ind in if Int.equal (Array.length mip.mind_consnames) 1 - && (allow_rec or not (mis_is_recursive (ind,mib,mip))) + && (allow_rec || not (mis_is_recursive (ind,mib,mip))) && (Int.equal mip.mind_nrealargs 0) then if is_strict_conjunction style (* strict conjunction *) then diff --git a/tactics/inv.ml b/tactics/inv.ml index ed22ab0e1..ec96a887d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -49,7 +49,7 @@ let check_no_metas clenv ccl = let var_occurs_in_pf gl id = let env = pf_env gl in - occur_var env id (pf_concl gl) or + occur_var env id (pf_concl gl) || List.exists (occur_var_in_decl env id) (pf_hyps gl) (* [make_inv_predicate (ity,args) C] diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index b397bcaa3..f0a757732 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -195,7 +195,7 @@ let intern_ltac_variable ist = function raise Not_found let intern_constr_reference strict ist = function - | Ident (_,id) as r when not strict & find_hyp id ist -> + | Ident (_,id) as r when not strict && find_hyp id ist -> GVar (dloc,id), Some (CRef r) | Ident (_,id) as r when find_ctxvar id ist -> GVar (dloc,id), if strict then None else Some (CRef r) @@ -361,7 +361,7 @@ let intern_evaluable_reference_or_by_notation ist = function (* Globalize a reduction expression *) let intern_evaluable ist = function | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id) - | AN (Ident (loc,id)) when not !strict_check & find_hyp id ist -> + | AN (Ident (loc,id)) when not !strict_check && find_hyp id ist -> ArgArg (EvalVarRef id, Some (loc,id)) | AN (Ident (loc,id)) when find_ctxvar id ist -> ArgArg (EvalVarRef id, if !strict_check then None else Some (loc,id)) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e97b01d38..4a60f6559 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -452,9 +452,9 @@ let build_intro_tac id dest tac = match dest with let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac gl = match kind_of_term (pf_concl gl) with - | Prod (name,t,u) when not dep_flag or (dependent (mkRel 1) u) -> + | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) -> build_intro_tac (find_name loc (name,None,t) gl name_flag) move_flag tac gl - | LetIn (name,b,t,u) when not dep_flag or (dependent (mkRel 1) u) -> + | LetIn (name,b,t,u) when not dep_flag || (dependent (mkRel 1) u) -> build_intro_tac (find_name loc (name,Some b,t) gl name_flag) move_flag tac gl | _ -> @@ -736,7 +736,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id c else clenv in let new_hyp_typ = clenv_type clenv in - if not with_evars & occur_meta new_hyp_typ then + if not with_evars && occur_meta new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in tclTHEN @@ -1142,8 +1142,8 @@ let (assumption : tactic) = fun gl -> | [] -> if only_eq then arec false hyps else error "No such assumption." | (id,c,t)::rest -> - if (only_eq & eq_constr t concl) - or (not only_eq & pf_conv_x_leq gl t concl) + if (only_eq && eq_constr t concl) + || (not only_eq && pf_conv_x_leq gl t concl) then refine_no_check (mkVar id) gl else arec only_eq rest in @@ -1231,8 +1231,8 @@ let keep hyps gl = let cl,_ = fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> if List.mem hyp hyps - or List.exists (occur_var_in_decl env hyp) keep - or occur_var env hyp ccl + || List.exists (occur_var_in_decl env hyp) keep + || occur_var env hyp ccl then (clear,decl::keep) else (hyp::clear,keep)) ~init:([],[]) (pf_env gl) @@ -1369,9 +1369,9 @@ let rewrite_hyp l2r id gl = (* TODO: detect setoid equality? better detect the different equalities *) match match_with_equality_type t with | Some (hdcncl,[_;lhs;rhs]) -> - if l2r & isVar lhs & not (occur_var (pf_env gl) (destVar lhs) rhs) then + if l2r && isVar lhs && not (occur_var (pf_env gl) (destVar lhs) rhs) then subst_on l2r (destVar lhs) rhs gl - else if not l2r & isVar rhs & not (occur_var (pf_env gl) (destVar rhs) lhs) then + else if not l2r && isVar rhs && not (occur_var (pf_env gl) (destVar rhs) lhs) then subst_on l2r (destVar rhs) lhs gl else tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl @@ -1602,7 +1602,7 @@ let generalize_dep ?(with_let=false) c gl = let init_ids = ids_of_named_context (Global.named_context()) in let seek d toquant = if List.exists (fun (id,_,_) -> occur_var_in_decl env id d) toquant - or dependent_in_decl c d then + || dependent_in_decl c d then d::toquant else toquant in @@ -1612,7 +1612,7 @@ let generalize_dep ?(with_let=false) c gl = let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in let tothin' = match kind_of_term c with - | Var id when mem_named_context id sign & not (List.mem id init_ids) + | Var id when mem_named_context id sign && not (List.mem id init_ids) -> id::tothin | _ -> tothin in @@ -2330,7 +2330,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 Int.equal n 1 (* Only one recursive argument *) or Int.equal n 0 then [] + if Int.equal n 1 (* Only one recursive argument *) || Int.equal n 0 then [] else (* Forbid to use cname, cname0, hyprecname and hyprecname0 *) (* in order to get names such as f1, f2, ... *) @@ -2787,7 +2787,7 @@ let compute_elim_sig ?elimc elimt = let hi_args_enough = (* hi a le bon nbre d'arguments *) Int.equal (List.length hi_args) (List.length params + !res.nargs -1) in (* FIXME: Ces deux tests ne sont pas suffisants. *) - if not (hi_is_ind & hi_args_enough) then raise Exit (* No indarg *) + if not (hi_is_ind && hi_args_enough) then raise Exit (* No indarg *) else (* Last arg is the indarg *) res := {!res with indarg = Some (List.hd !res.args); @@ -2826,14 +2826,14 @@ let compute_scheme_signature scheme names_info ind_type_guess = List.equal eq_constr (List.lastn scheme.nargs indargs) (extended_rel_list 0 scheme.args) in - if not (ccl_arg_ok & ind_is_ok) then + if not (ccl_arg_ok && ind_is_ok) then error_ind_scheme "the conclusion of" in (cond, check_concl) in let is_pred n c = let hd = fst (decompose_app c) in match kind_of_term hd with - | Rel q when n < q & q <= n+scheme.npredicates -> IndArg + | Rel q when n < q && q <= n+scheme.npredicates -> IndArg | _ when cond hd -> RecArg | _ -> OtherArg in @@ -3209,7 +3209,7 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc gl = | c::l' -> match kind_of_term c with | Var id when not (mem_named_context id (Global.named_context())) - & not with_evars -> + && not with_evars -> let _ = newlc:= id::!newlc in atomize_list l' gl @@ -3567,7 +3567,7 @@ let intros_transitivity n = tclTHEN intros (transitivity_gen n) let interpretable_as_section_decl d1 d2 = match d1,d2 with | (_,Some _,_), (_,None,_) -> false - | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 & eq_constr t1 t2 + | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 && eq_constr t1 t2 | (_,None,t1), (_,_,t2) -> eq_constr t1 t2 let abstract_subproof id tac gl = @@ -3576,7 +3576,7 @@ let abstract_subproof id tac gl = let sign,secsign = List.fold_right (fun (id,_,_ as d) (s1,s2) -> - if mem_named_context id current_sign & + if mem_named_context id current_sign && interpretable_as_section_decl (Context.lookup_named id current_sign) d then (s1,push_named_context_val d s2) else (add_named_decl d s1,s2)) diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 41b026c43..8c5e5b1ee 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -265,10 +265,10 @@ let escape = Buffer.clear s'; for i = 0 to String.length s - 1 do let c = s.[i] in - if c = ' ' or c = '#' or c = ':' (* separators and comments *) - or c = '%' (* pattern *) - or c = '?' or c = '[' or c = ']' or c = '*' (* expansion in filenames *) - or i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || + if c = ' ' || c = '#' || c = ':' (* separators and comments *) + || c = '%' (* pattern *) + || c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *) + || i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || 'A' <= s.[1] && s.[1] <= 'Z' || 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *) then begin diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 0ab732da2..0bcd44d0e 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -190,11 +190,11 @@ let parse_args () = | ("-no-start") :: rem -> no_start:=true; parse (op, fl) rem | f :: rem -> if Filename.check_suffix f ".ml" - or Filename.check_suffix f ".cmx" - or Filename.check_suffix f ".cmo" - or Filename.check_suffix f ".cmxa" - or Filename.check_suffix f ".cma" - or Filename.check_suffix f ".c" then + || Filename.check_suffix f ".cmx" + || Filename.check_suffix f ".cmo" + || Filename.check_suffix f ".cmxa" + || Filename.check_suffix f ".cma" + || Filename.check_suffix f ".c" then parse (op,f::fl) rem else begin prerr_endline ("Don't know what to do with " ^ f); diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index ee28156a3..0ca024ccb 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -86,7 +86,7 @@ let reset_input_buffer ic ibuf = let get_bols_of_loc ibuf (bp,ep) = let add_line (b,e) lines = - if b < 0 or e < b then anomaly (Pp.str "Bad location"); + if b < 0 || e < b then anomaly (Pp.str "Bad location"); match lines with | ([],None) -> ([], Some (b,e)) | (fl,oe) -> ((b,e)::fl, oe) @@ -181,7 +181,7 @@ let print_location_in_file {outer=s;inner=fname} loc = let valid_buffer_loc ib loc = not (Loc.is_ghost loc) && - let (b,e) = Loc.unloc loc in b-ib.start >= 0 & e-ib.start < ib.len && b<=e + let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e (*s The Coq prompt is the name of the focused proof, if any, and "Coq" otherwise. We trap all exceptions to prevent the error message printing diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 7508ffaab..887025418 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -57,8 +57,8 @@ let make_whelp_request req c = let b = Buffer.create 16 let url_char c = - if 'A' <= c & c <= 'Z' or 'a' <= c & c <= 'z' or - '0' <= c & c <= '9' or c ='.' + if 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' || + '0' <= c && c <= '9' || c ='.' then Buffer.add_char b c else Buffer.add_string b (Printf.sprintf "%%%2X" (Char.code c)) |