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

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))