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