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 | |
| 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')
| -rw-r--r-- | kernel/byterun/coq_memory.c | 14 | ||||
| -rw-r--r-- | kernel/byterun/coq_values.h | 13 |
2 files changed, 6 insertions, 21 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; 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 |