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/retroknowledge.ml b/kernel/retroknowledge.ml
index 48a6ff4c96..a84353bdc6 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -18,20 +18,24 @@ open Names
 
 type retroknowledge = {
     retro_int63 : Constant.t option;
+    retro_float64 : Constant.t option;
     retro_bool : (constructor * constructor) option; (* true, false *)
     retro_carry : (constructor * constructor) option; (* C0, C1 *)
     retro_pair : constructor option;
     retro_cmp : (constructor * constructor * constructor) option;
                     (* Eq, Lt, Gt *)
+    retro_option : (constructor * constructor) option; (* Some, None *)
     retro_refl : constructor option;
 }
 
 let empty = {
     retro_int63 = None;
+    retro_float64 = None;
     retro_bool = None;
     retro_carry = None;
     retro_pair = None;
     retro_cmp = None;
+    retro_option = None;
     retro_refl = None;
 }