diff options
Diffstat (limited to 'kernel/retroknowledge.mli')
| -rw-r--r-- | kernel/retroknowledge.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 0aca296d29..7aaf14e176 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -18,7 +18,9 @@ type retroknowledge = { retro_pair : constructor option; retro_cmp : (constructor * constructor * constructor) option; (* Eq, Lt, Gt *) - retro_option : (constructor * constructor) option; (* Some, None *) + retro_f_cmp : (constructor * constructor * constructor * constructor) + option; + (* FEq, FLt, FGt, FNotComparable *) retro_refl : constructor option; } |