diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2015-10-09 13:04:56 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-09 17:40:56 +0200 |
commit | c47b205206d832430fa80a3386be80149e281d33 (patch) | |
tree | a0556d85855e068235c5d91d2e909bf0a048a472 /kernel/byterun/coq_memory.c | |
parent | 7c82718f18afa3b317873f756a8801774ef64061 (diff) |
Code cleaning in VM (with Benjamin).
Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
Diffstat (limited to 'kernel/byterun/coq_memory.c')
-rw-r--r-- | kernel/byterun/coq_memory.c | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 8d03829ab..416e5e532 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -26,7 +26,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size; value coq_global_data; -int coq_all_transp; value coq_atom_tbl; int drawinstr; @@ -117,7 +116,6 @@ value init_coq_vm(value unit) /* ML */ init_coq_global_data(Coq_global_data_Size); init_coq_atom_tbl(40); /* Initialing the interpreter */ - coq_all_transp = 0; init_coq_interpreter(); /* Some predefined pointer code */ @@ -207,18 +205,6 @@ value realloc_coq_atom_tbl(value size) /* ML */ return Val_unit; } - -value coq_set_transp_value(value transp) -{ - coq_all_transp = (transp == Val_true); - return Val_unit; -} - -value get_coq_transp_value(value unit) -{ - return Val_bool(coq_all_transp); -} - value coq_set_drawinstr(value unit) { drawinstr = 1; |