aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/mfourier.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-03-01 18:26:26 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-03-01 22:45:39 +0100
commit87b510e5b0f363724eae5db9f177f167a3586015 (patch)
tree204c7ad1e1ba38945ab58d74e28d8cf67201fe71 /plugins/micromega/mfourier.ml
parentbca756eaebf16b6145c65b53629219d2a0a8b1ba (diff)
Fixing pervasive comparisons
Diffstat (limited to 'plugins/micromega/mfourier.ml')
-rw-r--r--plugins/micromega/mfourier.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index a1f08d568..7d08f2116 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -10,6 +10,8 @@ let from_option = Utils.from_option
let debug = false
type ('a,'b) lr = Inl of 'a | Inr of 'b
+let compare_float (p : float) q = Pervasives.compare p q
+
(** Implementation of intervals *)
module Itv =
struct
@@ -590,7 +592,7 @@ struct
(ISet.fold (fun v (eval,s) -> let ts,vl = abstract_partition v s in
((v,vl)::eval, ts)) v ([],sl)) in
- List.sort (fun x y -> Pervasives.compare (snd x) (snd y) ) evals
+ List.sort (fun x y -> compare_float (snd x) (snd y) ) evals
end
@@ -704,7 +706,7 @@ struct
(* pp_list (fun o ((v,eq,_,_),cst) -> Printf.fprintf o "((%i,%a),%i)\n" v pp_vect eq cst) stdout all_costs ; *)
- List.sort (fun x y -> Pervasives.compare (snd x) (snd y) ) all_costs
+ List.sort (fun x y -> Int.compare (snd x) (snd y) ) all_costs
| Some (v,vect, const,prf,_) -> [(v,vect,const,prf),0]