aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Benjamin Gregoire <Benjamin.Gregoire@inria.fr>2015-03-26 16:48:32 +0100
committerGravatar Benjamin Gregoire <Benjamin.Gregoire@inria.fr>2015-03-26 16:55:36 +0100
commitf920ae56ffacf80f85dcf33d3f1ccf0acb4375b1 (patch)
tree560d5f4ba0e9cc4cb0fbab3f1e1d9dc2b7706be2 /dev
parent5c6a50d6ec1d04bacd3e41ffbb88453fef92cd5d (diff)
fix compilation
Diffstat (limited to 'dev')
-rw-r--r--dev/vm_printers.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 4578a3b33..a583e2e54 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -74,14 +74,14 @@ and ppwhd whd =
| Vfix _ -> print_vfix()
| Vcofix _ -> print_string "cofix"
| Vconstr_const i -> print_string "C(";print_int i;print_string")"
- | Vconstr_block b -> ppvblock b
+ | Vconstr_block (tag,b) -> ppvblock tag b
| Vatom_stk(a,s) ->
open_hbox();ppatom a;close_box();
print_string"@";ppstack s
-and ppvblock b =
+and ppvblock tag b =
open_hbox();
- print_string "Cb(";print_int (btag b);
+ print_string "Cb(";print_int tag;
let n = bsize b in
for i = 0 to n -1 do
print_string ",";ppvalues (bfield b i)