diff options
| author | Guillaume Melquiond | 2020-08-26 13:37:20 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2020-11-13 15:13:23 +0100 |
| commit | 930e51c23f5a8778af02f7a971a404860d713346 (patch) | |
| tree | c82395fe93c70dd2e088b09958d27c7c42beb30c /kernel/vmemitcodes.ml | |
| parent | 51e759fb2ff92dd89ab4823ddea3ea81be7f8046 (diff) | |
Optimize handling of the VM stack with respect to the GC.
1. There is no point in marking plain integers as GC roots.
2. There is no need to restore the stack pointer, as the stack is not
allocated on the OCaml heap (contrarily to coq_env).
Diffstat (limited to 'kernel/vmemitcodes.ml')
0 files changed, 0 insertions, 0 deletions