diff options
Diffstat (limited to 'kernel/vmvalues.mli')
| -rw-r--r-- | kernel/vmvalues.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 1e40801be0..9c24006ff0 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -128,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 |