From fd5dc5b37e765bdb864e874c451d42d03d737792 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 3 Mar 2018 19:43:02 +0100
Subject: Moving the VM global atom table to a ML reference.

---
 kernel/vmvalues.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/vmvalues.mli')

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 =
-- 
cgit v1.2.3