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/vmvalues.mli | |
| parent | b5aed34bb8bbdda27646720db29a8d47c79653b9 (diff) | |
Moving the VM global atom table to a ML reference.
Diffstat (limited to 'kernel/vmvalues.mli')
| -rw-r--r-- | kernel/vmvalues.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 1fa889288..550791b2c 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -72,6 +72,9 @@ type atom = | Aind of inductive | Asort of Sorts.t +val get_atom_rel : unit -> atom array +(** Global table of rels *) + (** Zippers *) type zipper = |