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

12 files changed, 34 insertions, 34 deletions

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