diff options
Diffstat (limited to 'kernel/retroknowledge.ml')
| -rw-r--r-- | kernel/retroknowledge.ml | 10 |
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; } |