aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/vm_printers.ml
diff options
context:
space:
mode:
Diffstat (limited to 'dev/vm_printers.ml')
-rw-r--r--dev/vm_printers.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 16917586f..7589e5348 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -15,7 +15,10 @@ let ppripos (ri,pos) =
| Reloc_const _ ->
print_string "structured constant\n"
| Reloc_getglobal kn ->
- print_string ("getglob "^(Constant.to_string kn)^"\n"));
+ print_string ("getglob "^(Constant.to_string kn)^"\n")
+ | Reloc_proj_name p ->
+ print_string ("proj "^(Constant.to_string p)^"\n")
+ );
print_flush ()
let print_vfix () = print_string "vfix"