aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-09-19 12:59:04 +0000
committerGravatar xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-09-19 12:59:04 +0000
commit826eb7c6d11007dfd747d49852e71a22e0a3850a (patch)
tree25dce16a7107de4e0d3903e2808fb8f083d1f9ea
parent33eea163c72c70eaa3bf76506c1d07a8cde911fd (diff)
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
-rw-r--r--interp/constrextern.ml36
-rw-r--r--interp/constrintern.ml2
-rw-r--r--interp/notation.ml2
-rw-r--r--interp/notation_ops.ml12
-rw-r--r--interp/topconstr.ml2
-rw-r--r--kernel/cemitcodes.ml4
-rw-r--r--kernel/closure.ml8
-rw-r--r--kernel/constr.ml24
-rw-r--r--kernel/esubst.ml2
-rw-r--r--kernel/indtypes.ml2
-rw-r--r--kernel/inductive.ml2
-rw-r--r--kernel/term.ml2
-rw-r--r--kernel/vars.ml2
-rw-r--r--lib/bigint.ml44
-rw-r--r--lib/cArray.ml8
-rw-r--r--lib/cString.ml2
-rw-r--r--lib/hashcons.ml4
-rw-r--r--lib/hashset.ml4
-rw-r--r--lib/predicate.ml6
-rw-r--r--lib/profile.ml4
-rw-r--r--lib/unicode.ml4
-rw-r--r--lib/util.ml6
-rw-r--r--library/declare.ml2
-rw-r--r--library/goptions.ml2
-rw-r--r--library/heads.ml2
-rw-r--r--library/impargs.ml20
-rw-r--r--library/library.ml2
-rw-r--r--library/nameops.ml2
-rw-r--r--parsing/lexer.ml42
-rw-r--r--plugins/extraction/mlutil.ml2
-rw-r--r--plugins/fourier/fourierR.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml6
-rw-r--r--plugins/micromega/polynomial.ml2
-rw-r--r--plugins/nsatz/ideal.ml18
-rw-r--r--plugins/nsatz/utile.ml2
-rw-r--r--plugins/omega/coq_omega.ml2
-rw-r--r--plugins/omega/omega.ml14
-rw-r--r--plugins/quote/quote.ml8
-rw-r--r--plugins/romega/const_omega.ml2
-rw-r--r--plugins/syntax/ascii_syntax.ml2
-rw-r--r--plugins/syntax/r_syntax.ml8
-rw-r--r--pretyping/cases.ml4
-rw-r--r--pretyping/classops.ml2
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/detyping.ml12
-rw-r--r--pretyping/evarconv.ml6
-rw-r--r--pretyping/evarsolve.ml12
-rw-r--r--pretyping/glob_ops.ml14
-rw-r--r--pretyping/indrec.ml2
-rw-r--r--pretyping/matching.ml2
-rw-r--r--pretyping/namegen.ml8
-rw-r--r--pretyping/patternops.ml16
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--pretyping/recordops.ml2
-rw-r--r--pretyping/redops.ml2
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/retyping.ml2
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--pretyping/termops.ml6
-rw-r--r--pretyping/unification.ml2
-rw-r--r--printing/prettyp.ml2
-rw-r--r--printing/printer.ml2
-rw-r--r--proofs/logic.ml8
-rw-r--r--proofs/tactic_debug.ml2
-rw-r--r--tactics/auto.ml8
-rw-r--r--tactics/contradiction.ml2
-rw-r--r--tactics/eauto.ml42
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/hipattern.ml42
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/tacintern.ml4
-rw-r--r--tactics/tactics.ml36
-rw-r--r--tools/coqdep_common.ml8
-rw-r--r--tools/coqmktop.ml10
-rw-r--r--toplevel/toplevel.ml4
-rw-r--r--toplevel/whelp.ml44
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))