From c47b205206d832430fa80a3386be80149e281d33 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 9 Oct 2015 13:04:56 +0200 Subject: Code cleaning in VM (with Benjamin). Rename some functions, remove dead code related to (previously deprecated, now removed) option Set Boxed Values. --- kernel/byterun/coq_memory.c | 14 -------------- kernel/byterun/coq_values.h | 13 ++++++------- 2 files changed, 6 insertions(+), 21 deletions(-) (limited to 'kernel/byterun') 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; diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 1590a2141..80100da71 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -20,13 +20,12 @@ #define ATOM_ID_TAG 0 -#define ATOM_IDDEF_TAG 1 -#define ATOM_INDUCTIVE_TAG 2 -#define ATOM_PROJ_TAG 3 -#define ATOM_FIX_TAG 4 -#define ATOM_SWITCH_TAG 5 -#define ATOM_COFIX_TAG 6 -#define ATOM_COFIXEVALUATED_TAG 7 +#define ATOM_INDUCTIVE_TAG 1 +#define ATOM_PROJ_TAG 2 +#define ATOM_FIX_TAG 3 +#define ATOM_SWITCH_TAG 4 +#define ATOM_COFIX_TAG 5 +#define ATOM_COFIXEVALUATED_TAG 6 -- cgit v1.2.3