aboutsummaryrefslogtreecommitdiff
path: root/kernel/float64.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/float64.ml')
-rw-r--r--kernel/float64.ml9
1 files changed, 9 insertions, 0 deletions
diff --git a/kernel/float64.ml b/kernel/float64.ml
index 55ad472ea9..86b14c5cd2 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -42,6 +42,15 @@ let abs = abs_float
type float_comparison = FEq | FLt | FGt | FNotComparable
+let eq x y = x = y
+[@@ocaml.inline always]
+
+let lt x y = x < y
+[@@ocaml.inline always]
+
+let le x y = x <= y
+[@@ocaml.inline always]
+
(* inspired by lib/util.ml; see also #10471 *)
let pervasives_compare = compare