diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-02 15:41:50 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-26 08:57:39 +0200 |
| commit | b5aed34bb8bbdda27646720db29a8d47c79653b9 (patch) | |
| tree | ab5ca6003048afc0b8d0c2c4d9bce7e7a079cce2 /kernel/vmvalues.ml | |
| parent | e128900aee63c972d7977fd47e3fd21649b63409 (diff) | |
Moving the VM global data to a ML reference.
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 *** ************************) (*******************************************) |