Implement classify on primitive float

1 files changed, 9 insertions, 1 deletions

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;
 }