diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-03 19:43:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-26 08:57:39 +0200 |
| commit | fd5dc5b37e765bdb864e874c451d42d03d737792 (patch) | |
| tree | 464f48702d8b7116163f031a8f2c2bf2dec64823 /kernel/byterun/coq_memory.h | |
| parent | b5aed34bb8bbdda27646720db29a8d47c79653b9 (diff) | |
Moving the VM global atom table to a ML reference.
Diffstat (limited to 'kernel/byterun/coq_memory.h')
| -rw-r--r-- | kernel/byterun/coq_memory.h | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index 06711ad70..9375b15de 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -34,7 +34,6 @@ extern value * coq_stack_threshold; /* global_data */ extern int coq_all_transp; -extern value coq_atom_tbl; extern int drawinstr; /* interp state */ @@ -51,8 +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_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_ */ |