From e2e7fea91f3af5dcf62052078da65489b796e9e2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 31 Oct 2018 11:45:09 +0100
Subject: Pass native and VM flags to the kernel through environment

The kernel no longer has to read the configure flag, its value can now
be overriden by a coqtop/coqc argument, and more generally is easier to
set from a toplevel (such as the checker).

We also add a `-bytecode-compiler` flag.

Fixes #4607
---
 library/global.ml  | 3 +++
 library/global.mli | 3 +++
 2 files changed, 6 insertions(+)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index bfea6d3dea..4ea5969a6f 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -186,3 +186,6 @@ let set_strategy k l =
 
 let set_share_reduction b =
   globalize0 (Safe_typing.set_share_reduction b)
+
+let set_VM b = globalize0 (Safe_typing.set_VM b)
+let set_native_compiler b = globalize0 (Safe_typing.set_native_compiler b)
diff --git a/library/global.mli b/library/global.mli
index 762a3f006d..01ee695c49 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -154,6 +154,9 @@ val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
 
 val set_share_reduction : bool -> unit
 
+val set_VM : bool -> unit
+val set_native_compiler : bool -> unit
+
 (* Modifies the global state, registering new universes *)
 
 val current_modpath : unit -> ModPath.t
-- 
cgit v1.2.3