From b5aed34bb8bbdda27646720db29a8d47c79653b9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 2 Mar 2018 15:41:50 +0100
Subject: Moving the VM global data 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 c6e342a965..1fa889288b 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -15,6 +15,7 @@ open Cbytecodes
 
 type values
 type vm_env
+type vm_global
 type vprod
 type vfun
 type vfix
@@ -33,6 +34,8 @@ val fix_env : vfix -> vm_env
 val cofix_env : vcofix -> vm_env
 val cofix_upd_env : to_update -> vm_env
 
+val vm_global : values array -> vm_global
+
 (** Cast a value known to be a function, unsafe in general *)
 val fun_of_val : values -> vfun
 
-- 
cgit v1.2.3


From fd5dc5b37e765bdb864e874c451d42d03d737792 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
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 1fa889288b..550791b2c8 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