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
---
 checker/cic.mli   | 2 ++
 checker/values.ml | 4 ++--
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'checker')

diff --git a/checker/cic.mli b/checker/cic.mli
index 4162903b04..754cc2a096 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -221,6 +221,8 @@ type typing_flags = {
   check_universes : bool; (** If [false] universe constraints are not checked *)
   conv_oracle : oracle; (** Unfolding strategies for conversion *)
   share_reduction : bool; (** Use by-need reduction algorithm *)
+  enable_VM : bool; (** If [false], all VM conversions fall back to interpreted ones *)
+  enable_native_compiler : bool; (** If [false], all native conversions fall back to VM ones *)
 }
 
 type constant_body = {
diff --git a/checker/values.ml b/checker/values.ml
index 24f10b7a87..8f6b24ec26 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 a127e0c2322c7846914bbca9921309c7 checker/cic.mli
+MD5 b8f0139f14e3370cd0a45d4cf69882ea checker/cic.mli
 
 *)
 
@@ -230,7 +230,7 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool|]
+  v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool|]
 
 let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 
-- 
cgit v1.2.3