aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/sos_lib.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/sos_lib.ml
parentbca756eaebf16b6145c65b53629219d2a0a8b1ba (diff)
Fixing pervasive comparisons
Diffstat (limited to 'plugins/micromega/sos_lib.ml')
-rw-r--r--plugins/micromega/sos_lib.ml12
1 files changed, 7 insertions, 5 deletions
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index efb3f9885..235f9ce9b 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -15,11 +15,13 @@ let debugging = ref false;;
(* Comparisons that are reflexive on NaN and also short-circuiting. *)
(* ------------------------------------------------------------------------- *)
-let (=?) = fun x y -> Pervasives.compare x y = 0;;
-let (<?) = fun x y -> Pervasives.compare x y < 0;;
-let (<=?) = fun x y -> Pervasives.compare x y <= 0;;
-let (>?) = fun x y -> Pervasives.compare x y > 0;;
-let (>=?) = fun x y -> Pervasives.compare x y >= 0;;
+let cmp = Pervasives.compare (** FIXME *)
+
+let (=?) = fun x y -> cmp x y = 0;;
+let (<?) = fun x y -> cmp x y < 0;;
+let (<=?) = fun x y -> cmp x y <= 0;;
+let (>?) = fun x y -> cmp x y > 0;;
+let (>=?) = fun x y -> cmp x y >= 0;;
(* ------------------------------------------------------------------------- *)
(* Combinators. *)