diff options
Diffstat (limited to 'kernel/retroknowledge.ml')
| -rw-r--r-- | kernel/retroknowledge.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index a84353bdc6..e897be6141 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -24,7 +24,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; } @@ -35,7 +37,7 @@ let empty = { retro_carry = None; retro_pair = None; retro_cmp = None; - retro_option = None; + retro_f_cmp = None; retro_refl = None; } |