diff options
| author | Maxime Dénès | 2018-04-20 17:17:04 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-04-20 17:17:04 +0200 |
| commit | 239e28f71192d7537bc6ea283c806ba28fa1c016 (patch) | |
| tree | 66332e6670c648a73284bc97ed36b6174a8002f6 /kernel/byterun/coq_memory.h | |
| parent | 350ee43d73ee4d6c9b6c3fd24cae3aca8a2b5ce4 (diff) | |
| parent | 93c8e14d0c9bc233b2dcf213485b62a533b34580 (diff) | |
Merge PR #6908: Move VM global tables from C to ML
Diffstat (limited to 'kernel/byterun/coq_memory.h')
| -rw-r--r-- | kernel/byterun/coq_memory.h | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index cec34f566c..9375b15de2 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -20,7 +20,6 @@ #define Coq_stack_size (4096 * sizeof(value)) #define Coq_stack_threshold (256 * sizeof(value)) -#define Coq_global_data_Size (4096 * sizeof(value)) #define Coq_max_stack_size (256 * 1024) #define TRANSP 0 @@ -34,9 +33,7 @@ extern value * coq_stack_threshold; /* global_data */ -extern value coq_global_data; extern int coq_all_transp; -extern value coq_atom_tbl; extern int drawinstr; /* interp state */ @@ -53,10 +50,6 @@ value init_coq_vm(value unit); /* ML */ value re_init_coq_vm(value unit); /* ML */ void realloc_coq_stack(asize_t required_space); -value get_coq_global_data(value unit); /* ML */ -value realloc_coq_global_data(value size); /* ML */ -value get_coq_atom_tbl(value unit); /* ML */ -value realloc_coq_atom_tbl(value size); /* ML */ value coq_set_transp_value(value transp); /* ML */ value get_coq_transp_value(value unit); /* ML */ #endif /* _COQ_MEMORY_ */ |