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
---
 kernel/safe_typing.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 443b5cfd73..8fb33b04d4 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -138,6 +138,8 @@ val add_constraints :
 val set_engagement : Declarations.engagement -> safe_transformer0
 val set_typing_flags : Declarations.typing_flags -> safe_transformer0
 val set_share_reduction : bool -> safe_transformer0
+val set_VM : bool -> safe_transformer0
+val set_native_compiler : bool -> safe_transformer0
 
 (** {6 Interactive module functions } *)
 
-- 
cgit v1.2.3