diff options
Diffstat (limited to 'kernel/vmvalues.mli')
| -rw-r--r-- | kernel/vmvalues.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index d289e7db9a..9c24006ff0 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -45,6 +45,7 @@ type structured_constant = | Const_univ_level of Univ.Level.t | Const_val of structured_values | Const_uint of Uint63.t + | Const_float of Float64.t val pp_struct_const : structured_constant -> Pp.t @@ -127,6 +128,7 @@ type whd = | Vconstr_const of int | Vconstr_block of vblock | Vint64 of int64 + | Vfloat64 of float | Vatom_stk of atom * stack | Vuniv_level of Univ.Level.t |