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

4 files changed, 15 insertions, 15 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