Add primitive float computation in Coq kernel

Beware of 0. = -0. issue for primitive floats

The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.

1 files changed, 4 insertions, 0 deletions

diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index d22ba3468f..c7d1e36451 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -21,6 +21,10 @@ val of_int64 : Int64.t -> t
 val of_uint : int -> t
 *)
 
+      (* conversion to float *)
+val of_float : float -> t
+val to_float : t -> float
+
 val hash : t -> int
 
      (* conversion to a string *)