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

9 files changed, 41 insertions, 41 deletions

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