From 6133877fc097412233a60740fdf94374abb79559 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Wed, 20 Feb 2019 18:00:04 +0100
Subject: Add primitive floats to checker

---
 kernel/float64.ml  | 11 +++++++++--
 kernel/float64.mli |  3 +++
 2 files changed, 12 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/float64.ml b/kernel/float64.ml
index c0611f37a0..72f0d83359 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -35,6 +35,9 @@ let abs = abs_float
 
 type float_comparison = FEq | FLt | FGt | FNotComparable
 
+(* inspired by lib/util.ml; see also #10471 *)
+let pervasives_compare = compare
+
 let compare x y =
   if x < y then FLt
   else
@@ -137,5 +140,9 @@ let hash =
 let total_compare f1 f2 =
   (* pervasives_compare considers all NaNs as equal, which is fine here,
      but also considers -0. and +0. as equal *)
-  if f1 = 0. && f2 = 0. then Util.pervasives_compare (1. /. f1) (1. /. f2)
-  else Util.pervasives_compare f1 f2
+  if f1 = 0. && f2 = 0. then pervasives_compare (1. /. f1) (1. /. f2)
+  else pervasives_compare f1 f2
+
+let is_float64 t =
+  Obj.tag t = Obj.double_tag
+[@@ocaml.inline always]
diff --git a/kernel/float64.mli b/kernel/float64.mli
index 1e6ea8bb96..927594115e 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -87,3 +87,6 @@ val hash : t -> int
 
 (** Total order relation over float values. Behaves like [Pervasives.compare].*)
 val total_compare : t -> t -> int
+
+val is_float64 : Obj.t -> bool
+[@@ocaml.inline always]
-- 
cgit v1.2.3