diff options
author | xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-19 12:59:04 +0000 |
---|---|---|
committer | xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-19 12:59:04 +0000 |
commit | 826eb7c6d11007dfd747d49852e71a22e0a3850a (patch) | |
tree | 25dce16a7107de4e0d3903e2808fb8f083d1f9ea /plugins/omega/omega.ml | |
parent | 33eea163c72c70eaa3bf76506c1d07a8cde911fd (diff) |
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
Diffstat (limited to 'plugins/omega/omega.ml')
-rw-r--r-- | plugins/omega/omega.ml | 14 |
1 files changed, 7 insertions, 7 deletions
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 |