diff options
Diffstat (limited to 'dev/vm_printers.ml')
| -rw-r--r-- | dev/vm_printers.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 863d930968..73cf1b0195 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -51,7 +51,7 @@ let rec ppzipper z = let n = nargs args in open_hbox (); for i = 0 to n-2 do - ppvalues (arg args i);print_string ";";print_space() + ppvalues (arg args i);print_string ";";print_space() done; if n-1 >= 0 then ppvalues (arg args (n-1)); close_box() @@ -84,6 +84,7 @@ and ppwhd whd = | Vconstr_const i -> print_string "C(";print_int i;print_string")" | Vconstr_block b -> ppvblock b | Vint64 i -> printf "int64(%LiL)" i + | Vfloat64 f -> printf "float64(%.17g)" f | Vatom_stk(a,s) -> open_hbox();ppatom a;close_box(); print_string"@";ppstack s |