From b0b3cc67e01b165272588b2d8bc178840ba83945 Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Fri, 13 Jul 2018 16:22:35 +0200
Subject: 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.
---
 dev/top_printers.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index aa28bce018..ccb8658eee 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -307,6 +307,8 @@ let constr_display csr =
       ^(array_display bl)^")"
   | Int i ->
       "Int("^(Uint63.to_string i)^")"
+  | Float f ->
+      "Float("^(Float64.to_string f)^")"
 
   and array_display v =
     "[|"^
@@ -439,6 +441,8 @@ let print_pure_constr csr =
       in print_string"{"; print_fix (); print_string"}"
   | Int i ->
      print_string ("Int("^(Uint63.to_string i)^")")
+  | Float f ->
+      print_string ("Float("^(Float64.to_string f)^")")
 
   and box_display c = open_hovbox 1; term_display c; close_box()
 
-- 
cgit v1.2.3