diff options
Diffstat (limited to 'kernel/vmvalues.ml')
| -rw-r--r-- | kernel/vmvalues.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 0e0cb4e58..6377e947f 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -43,6 +43,7 @@ let fix_val v = (Obj.magic v : values) let cofix_upd_val v = (Obj.magic v : values) type vm_env +type vm_global let fun_env v = (Obj.magic v : vm_env) let fix_env v = (Obj.magic v : vm_env) let cofix_env v = (Obj.magic v : vm_env) @@ -51,6 +52,8 @@ type vstack = values array let fun_of_val v = (Obj.magic v : vfun) +let vm_global (v : values array) = (Obj.magic v : vm_global) + (*******************************************) (* Machine code *** ************************) (*******************************************) |