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.
---
 kernel/vmvalues.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/vmvalues.mli')

diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index d289e7db9a..1e40801be0 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -45,6 +45,7 @@ type structured_constant =
   | Const_univ_level of Univ.Level.t
   | Const_val of structured_values
   | Const_uint of Uint63.t
+  | Const_float of Float64.t
 
 val pp_struct_const : structured_constant -> Pp.t
 
-- 
cgit v1.2.3


From cc7dfa82705b64d1cf43408244ef6c7dd930a6e9 Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Thu, 19 Jul 2018 13:33:17 +0200
Subject: Add primitive floats to 'vm_compute'

* This commit add float instructions to the VM, their encoding in bytecode
  and the interpretation of primitive float values after the reduction.

* The flag '-std=c99' could be added to the C compiler flags to ensure
  that float computation strictly follows the norm (ie. i387 80-bits
  format is not used as an optimization).

  Actually, we use '-fexcess-precision=standard' instead of '-std=c99'
  because the latter would disable GNU asm used in the VM.
---
 kernel/vmvalues.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/vmvalues.mli')

diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 1e40801be0..9c24006ff0 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -128,6 +128,7 @@ type whd =
   | Vconstr_const of int
   | Vconstr_block of vblock
   | Vint64 of int64
+  | Vfloat64 of float
   | Vatom_stk of atom * stack
   | Vuniv_level of Univ.Level.t
 
-- 
cgit v1.2.3