aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--dev/vm_printers.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 4578a3b33..3d688011c 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -49,6 +49,7 @@ let rec ppzipper z =
close_box()
| Zfix _ -> print_string "Zfix"
| Zswitch _ -> print_string "Zswitch"
+ | Zproj _ -> print_string "Zproj"
and ppstack s =
open_hovbox 0;