diff options
Diffstat (limited to 'kernel/retroknowledge.ml')
| -rw-r--r-- | kernel/retroknowledge.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 48a6ff4c96..a84353bdc6 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -18,20 +18,24 @@ open Names type retroknowledge = { retro_int63 : Constant.t option; + retro_float64 : Constant.t option; retro_bool : (constructor * constructor) option; (* true, false *) retro_carry : (constructor * constructor) option; (* C0, C1 *) retro_pair : constructor option; retro_cmp : (constructor * constructor * constructor) option; (* Eq, Lt, Gt *) + retro_option : (constructor * constructor) option; (* Some, None *) retro_refl : constructor option; } let empty = { retro_int63 = None; + retro_float64 = None; retro_bool = None; retro_carry = None; retro_pair = None; retro_cmp = None; + retro_option = None; retro_refl = None; } |