From 826eb7c6d11007dfd747d49852e71a22e0a3850a Mon Sep 17 00:00:00 2001
From: xclerc
Date: Thu, 19 Sep 2013 12:59:04 +0000
Subject: 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
---
 plugins/omega/coq_omega.ml |  2 +-
 plugins/omega/omega.ml     | 14 +++++++-------
 2 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'plugins/omega')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index f98aba0a89..0dd137b6f5 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 800254671f..60887b4511 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
-- 
cgit v1.2.3