diff options
Diffstat (limited to 'dev/vm_printers.ml')
| -rw-r--r-- | dev/vm_printers.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index c037eca7..1e114489 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -65,8 +65,6 @@ and ppatom a = print_string (string_of_kn sp); print_string ","; print_int i; print_string ")" - | Afix_app _ -> print_vfix_app () - | Aswitch _ -> print_vswith() and ppwhd whd = match whd with @@ -74,9 +72,7 @@ and ppwhd whd = | Vprod _ -> print_string "product" | Vfun _ -> print_string "function" | Vfix _ -> print_vfix() - | Vfix_app _ -> print_vfix_app() | Vcofix _ -> print_string "cofix" - | Vcofix_app _ -> print_string "cofix_app" | Vconstr_const i -> print_string "C(";print_int i;print_string")" | Vconstr_block b -> ppvblock b | Vatom_stk(a,s) -> |