From f93684a412f067622a5026c406bc76032c30b6e9 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 2 Apr 2019 22:39:32 +0200
Subject: Declare type of primitives in CPrimitives

Rather than in typeops
---
 kernel/retroknowledge.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/retroknowledge.ml')

diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 873c6af93d..48a6ff4c96 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -36,5 +36,5 @@ let empty = {
 }
 
 type action =
-  | Register_ind of CPrimitives.prim_ind * inductive
-  | Register_type of CPrimitives.prim_type * Constant.t
+  | Register_ind : 'a CPrimitives.prim_ind * inductive -> action
+  | Register_type : CPrimitives.prim_type * Constant.t -> action
-- 
cgit v1.2.3


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/retroknowledge.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/retroknowledge.ml')

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;
 }
 
-- 
cgit v1.2.3


From 79605dabb10e889ae998bf72c8483f095277e693 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 28 Aug 2018 14:31:37 +0200
Subject: Change return type of primitive float comparison

Replace `option comparison` with `float_comparison` (:= `FEq | FLt |
FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid
boxing and an extra match when using primitive float comparison.
---
 kernel/retroknowledge.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel/retroknowledge.ml')

diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index a84353bdc6..e897be6141 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -24,7 +24,9 @@ type retroknowledge = {
     retro_pair : constructor option;
     retro_cmp : (constructor * constructor * constructor) option;
                     (* Eq, Lt, Gt *)
-    retro_option : (constructor * constructor) option; (* Some, None *)
+    retro_f_cmp : (constructor * constructor * constructor * constructor)
+                  option;
+                  (* FEq, FLt, FGt, FNotComparable *)
     retro_refl : constructor option;
 }
 
@@ -35,7 +37,7 @@ let empty = {
     retro_carry = None;
     retro_pair = None;
     retro_cmp = None;
-    retro_option = None;
+    retro_f_cmp = None;
     retro_refl = None;
 }
 
-- 
cgit v1.2.3


From d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 28 Aug 2018 18:56:07 +0200
Subject: Implement classify on primitive float

---
 kernel/retroknowledge.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'kernel/retroknowledge.ml')

diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index e897be6141..479fe02295 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -27,7 +27,14 @@ type retroknowledge = {
     retro_f_cmp : (constructor * constructor * constructor * constructor)
                   option;
                   (* FEq, FLt, FGt, FNotComparable *)
-    retro_refl : constructor option;
+    retro_f_class : (constructor * constructor * constructor * constructor
+                     * constructor * constructor * constructor * constructor
+                     * constructor)
+                      option;
+                    (* PNormal, NNormal, PSubn, NSubn,
+                       PZero, NZero, PInf, NInf,
+                       NaN *)
+    retro_refl : constructor option
 }
 
 let empty = {
@@ -38,6 +45,7 @@ let empty = {
     retro_pair = None;
     retro_cmp = None;
     retro_f_cmp = None;
+    retro_f_class = None;
     retro_refl = None;
 }
 
-- 
cgit v1.2.3