diff options
Diffstat (limited to 'kernel/vmbytecodes.ml')
| -rw-r--r-- | kernel/vmbytecodes.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml index c2b087f061..1783560694 100644 --- a/kernel/vmbytecodes.ml +++ b/kernel/vmbytecodes.ml @@ -35,6 +35,7 @@ type instruction = | Kpush | Kpop of int | Kpush_retaddr of Label.t + | Kshort_apply of int | Kapply of int | Kappterm of int * int | Kreturn of int @@ -93,6 +94,7 @@ let rec pp_instr i = | Kpush -> str "push" | Kpop n -> str "pop " ++ int n | Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl + | Kshort_apply n -> str "short_apply " ++ int n | Kapply n -> str "apply " ++ int n | Kappterm(n, m) -> str "appterm " ++ int n ++ str ", " ++ int m |