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

8 files changed, 23 insertions, 23 deletions

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