diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
| commit | 1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch) | |
| tree | 5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /kernel/byterun/coq_memory.h | |
| parent | 3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff) | |
| parent | 9ebf44d84754adc5b64fcf612c6816c02c80462d (diff) | |
Updated version 8.9.0 from 'upstream/8.9.0'
with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63
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 cec34f56..9375b15d 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_ */ |