diff options
Diffstat (limited to 'kernel/retroknowledge.mli')
| -rw-r--r-- | kernel/retroknowledge.mli | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 2a7b390951..2df8a00465 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -12,16 +12,27 @@ 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_refl : constructor option; + retro_f_cmp : (constructor * constructor * constructor * constructor) + option; + (* FEq, FLt, FGt, FNotComparable *) + 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 type action = - | Register_ind of CPrimitives.prim_ind * inductive - | Register_type of CPrimitives.prim_type * Constant.t + | Register_ind : 'a CPrimitives.prim_ind * inductive -> action + | Register_type : CPrimitives.prim_type * Constant.t -> action |