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.mli | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'kernel/retroknowledge.mli')

diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 7aaf14e176..2df8a00465 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -21,7 +21,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
 }
 
 val empty : retroknowledge
-- 
cgit v1.2.3