From ec5ed7870b4b59e05c5e994c9bad35e28685b8bd Mon Sep 17 00:00:00 2001
From: xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 14 Oct 2013 07:33:57 +0000
Subject: Getting rid of the use of deprecated elements (from the OCaml
 standard library).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/closure.ml           | 10 +++++-----
 checker/declarations.ml      |  2 +-
 checker/inductive.ml         | 16 ++++++++--------
 checker/reduction.ml         |  2 +-
 plugins/micromega/sos.ml     | 24 ++++++++++++------------
 plugins/micromega/sos_lib.ml |  6 +++---
 tools/coq_makefile.ml        |  8 ++++----
 tools/coq_tex.ml             |  2 +-
 tools/coqdoc/index.ml        |  2 +-
 9 files changed, 36 insertions(+), 36 deletions(-)

diff --git a/checker/closure.ml b/checker/closure.ml
index 3ed9dd27a..55c91b93e 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -345,7 +345,7 @@ let compact_stack head stk =
 
 (* Put an update mark in the stack, only if needed *)
 let zupdate m s =
-  if !share & m.norm = Red
+  if !share && m.norm = Red
   then
     let s' = compact_stack m s in
     let _ = m.term <- FLOCKED in
@@ -541,11 +541,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 -> Fix fx
-      | FCoFix(cfx,e) when is_subs_id e & is_lift_id lfts -> CoFix cfx
+      | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> Fix fx
+      | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> CoFix cfx
       | _ -> to_constr term_of_fconstr_lift lfts v in
   term_of_fconstr_lift el_id
 
diff --git a/checker/declarations.ml b/checker/declarations.ml
index a6a7f9405..dfa7d401e 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -446,7 +446,7 @@ let is_opaque cb = match cb.const_body with
 let subst_rel_declaration sub (id,copt,t as x) =
   let copt' = Option.smartmap (subst_mps sub) copt in
   let t' = subst_mps sub t in
-  if copt == copt' & t == t' then x else (id,copt',t')
+  if copt == copt' && t == t' then x else (id,copt',t')
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 9e1524018..2dd76c4d3 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -345,8 +345,8 @@ let type_case_branches env (ind,largs) (p,pj) c =
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
-    not (eq_ind indsp ci.ci_ind) or
-    (mib.mind_nparams <> ci.ci_npar) or
+    not (eq_ind indsp ci.ci_ind) ||
+    (mib.mind_nparams <> ci.ci_npar) ||
     (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls)
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
 
@@ -657,7 +657,7 @@ let check_one_fix renv recpos def =
       match 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: *)
@@ -779,11 +779,11 @@ let check_one_fix renv recpos def =
 let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   let nbfix = Array.length bodies in
   if nbfix = 0
-    or Array.length nvect <> nbfix
-    or Array.length types <> nbfix
-    or Array.length names <> nbfix
-    or bodynum < 0
-    or bodynum >= nbfix
+    || Array.length nvect <> nbfix
+    || Array.length types <> nbfix
+    || Array.length names <> nbfix
+    || bodynum < 0
+    || bodynum >= nbfix
   then anomaly (Pp.str "Ill-formed fix term");
   let fixenv = push_rec_types recdef env in
   let raise_err env i err =
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 53a12295e..e07a3128b 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -144,7 +144,7 @@ type conv_pb =
 
 let sort_cmp univ pb s0 s1 =
   match (s0,s1) with
-    | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos & c2 = Null then raise NotConvertible
+    | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible
     | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
     | (Prop c1, Type u)  ->
         (match pb with
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index 130f6bfd4..6816abb2f 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -200,11 +200,11 @@ let monomial_pow (m:monomial) k =
   else mapf (fun x -> k * x) m;;
 
 let monomial_divides (m1:monomial) (m2:monomial) =
-  foldl (fun a x k -> tryapplyd m2 x 0 >= k & a) true m1;;
+  foldl (fun a x k -> tryapplyd m2 x 0 >= k && a) true m1;;
 
 let monomial_div (m1:monomial) (m2:monomial) =
   let m = combine (+) (fun x -> x = 0) m1 (mapf (fun x -> -x) m2) in
-  if foldl (fun a x k -> k >= 0 & a) true m then m
+  if foldl (fun a x k -> k >= 0 && a) true m then m
   else failwith "monomial_div: non-divisible";;
 
 let monomial_degree x (m:monomial) = tryapplyd m x 0;;
@@ -226,7 +226,7 @@ let eval assig (p:poly) =
 
 let poly_0 = (undefined:poly);;
 
-let poly_isconst (p:poly) = foldl (fun a m c -> m = monomial_1 & a) true p;;
+let poly_isconst (p:poly) = foldl (fun a m c -> m = monomial_1 && a) true p;;
 
 let poly_var x = ((monomial_var x) |=> Int 1 :poly);;
 
@@ -282,14 +282,14 @@ let poly_variables (p:poly) =
 (* Order monomials for human presentation.                                   *)
 (* ------------------------------------------------------------------------- *)
 
-let humanorder_varpow (x1,k1) (x2,k2) = x1 < x2 or x1 = x2 & k1 > k2;;
+let humanorder_varpow (x1,k1) (x2,k2) = x1 < x2 || x1 = x2 && k1 > k2;;
 
 let humanorder_monomial =
   let rec ord l1 l2 = match (l1,l2) with
     _,[] -> true
   | [],_ -> false
-  | h1::t1,h2::t2 -> humanorder_varpow h1 h2 or h1 = h2 & ord t1 t2 in
-  fun m1 m2 -> m1 = m2 or
+  | h1::t1,h2::t2 -> humanorder_varpow h1 h2 || h1 = h2 && ord t1 t2 in
+  fun m1 m2 -> m1 = m2 ||
                ord (sort humanorder_varpow (graph m1))
                    (sort humanorder_varpow (graph m2));;
 
@@ -602,7 +602,7 @@ let run_csdp dbg obj mats =
 
 let csdp obj mats =
   let rv,res = run_csdp (!debugging) obj mats in
-  (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible"
+  (if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible"
    else if rv = 3 then ()
     (* Format.print_string "csdp warning: Reduced accuracy";
      Format.print_newline() *)
@@ -653,7 +653,7 @@ let linear_program_basic a =
   let mats =  List.map (fun j -> diagonal (column j a)) (1--n)
   and obj = vector_const (Int 1) m in
   let rv,res = run_csdp false obj mats in
-  if rv = 1 or rv = 2 then false
+  if rv = 1 || rv = 2 then false
   else if rv = 0 then true
   else failwith "linear_program: An error occurred in the SDP solver";;
 
@@ -667,7 +667,7 @@ let linear_program a b =
   let mats = diagonal b :: List.map (fun j -> diagonal (column j a)) (1--n)
   and obj = vector_const (Int 1) m in
   let rv,res = run_csdp false obj mats in
-  if rv = 1 or rv = 2 then false
+  if rv = 1 || rv = 2 then false
   else if rv = 0 then true
   else failwith "linear_program: An error occurred in the SDP solver";;
 
@@ -968,7 +968,7 @@ let run_csdp dbg nblocks blocksizes obj mats =
 
 let csdp nblocks blocksizes obj mats =
   let rv,res = run_csdp (!debugging) nblocks blocksizes obj mats in
-  (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible"
+  (if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible"
    else if rv = 3 then ()
     (*Format.print_string "csdp warning: Reduced accuracy";
      Format.print_newline() *)
@@ -1052,7 +1052,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol =
                                 ((b,j,i) |-> c) (((b,i,j) |-> c) m))
           undefined allassig in
   let diagents = foldl
-    (fun a (b,i,j) e -> if b > 0 & i = j then equation_add e a else a)
+    (fun a (b,i,j) e -> if b > 0 && i = j then equation_add e a else a)
     undefined allassig in
   let mats = List.map mk_matrix qvars
   and obj = List.length pvs,
@@ -1439,7 +1439,7 @@ let run_csdp dbg obj mats =
 
 let csdp obj mats =
   let rv,res = run_csdp (!debugging) obj mats in
-  (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible"
+  (if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible"
     else if rv = 3 then ()
 (*    (Format.print_string "csdp warning: Reduced accuracy";
      Format.print_newline()) *)
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index 41cbeda3f..efb3f9885 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -52,7 +52,7 @@ let gcd_num n1 n2 =
   num_of_big_int(Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2));;
 
 let lcm_num x y =
-  if x =/ num_0 & y =/ num_0 then num_0
+  if x =/ num_0 && y =/ num_0 then num_0
   else abs_num((x */ y) // gcd_num x y);;
 
 
@@ -140,7 +140,7 @@ let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);;
 let rec forall p l =
   match l with
     [] -> true
-  | h::t -> p(h) & forall p t;;
+  | h::t -> p(h) && forall p t;;
 
 let rec tryfind f l =
   match l with
@@ -161,7 +161,7 @@ let index x =
 let rec mem x lis =
   match lis with
     [] -> false
-  | (h::t) -> x =? h or mem x t;;
+  | (h::t) -> x =? h || mem x t;;
 
 let insert x l =
   if mem x l then l else x::l;;
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 060bd3d37..bd77bb1ba 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -89,7 +89,7 @@ let string_prefix a b =
 let is_prefix dir1 dir2 =
   let l1 = String.length dir1 in
   let l2 = String.length dir2 in
-    dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/')
+    dir1 = dir2 || (l1 < l2 && String.sub dir2 0 l1 = dir1 && dir2.[l1] = '/')
 
 let physical_dir_of_logical_dir ldir =
   let le = String.length ldir - 1 in
@@ -687,8 +687,8 @@ let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((i_inc,r_inc) as l) =
   let here = Sys.getcwd () in
   let not_tops =List.for_all (fun s -> s <> Filename.basename s) in
   if List.exists (fun (_,x) -> x = here) i_inc
-    or List.exists (fun (_,_,x) -> is_prefix x here) r_inc
-    or (not_tops v && not_tops mli && not_tops ml4 && not_tops ml
+    || List.exists (fun (_,_,x) -> is_prefix x here) r_inc
+    || (not_tops v && not_tops mli && not_tops ml4 && not_tops ml
 	&& not_tops mllib && not_tops mlpack) then
     l
   else
@@ -712,7 +712,7 @@ let check_overlapping_include (_,inc_r) =
 	if not (is_prefix pwd abspdir) then
 	  Printf.eprintf "Warning: in option -R, %s is not a subdirectory of the current directory\n" pdir;
 	List.iter (fun (pdir',_,abspdir') ->
-	  if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then
+	  if is_prefix abspdir abspdir' || is_prefix abspdir' abspdir then
 	    Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l;
   in aux inc_r
 
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index c19a9c3f1..c47be6e77 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -171,7 +171,7 @@ let insert texfile coq_output result =
       just_after ()
     end else begin
       if !verbose then Printf.printf "Coq < %s\n" s;
-      if (not first_block) & k=0 then output_string c_out "\\medskip\n";
+      if (not first_block) && k=0 then output_string c_out "\\medskip\n";
       if show_questions then encapsule false c_out ("Coq < " ^ s);
       if has_match dot_end_line s then begin
 	let bl = next_block (succ k) in
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 7368ac1e0..8e82f4577 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -131,7 +131,7 @@ let find_external_library logicalpath =
   let rec aux = function
     | [] -> raise Not_found
     | (l,u)::rest ->
-        if String.length logicalpath > String.length l &
+        if String.length logicalpath > String.length l &&
           String.sub logicalpath 0 (String.length l + 1) = l ^"."
         then u
         else aux rest
-- 
cgit v1.2.3