diff options
Diffstat (limited to 'kernel/retroknowledge.mli')
| -rw-r--r-- | kernel/retroknowledge.mli | 9 |
1 files changed, 8 insertions, 1 deletions
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 |