diff options
| author | Maxime Dénès | 2018-10-31 11:45:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-05 10:36:22 +0100 |
| commit | e2e7fea91f3af5dcf62052078da65489b796e9e2 (patch) | |
| tree | d44da683ff0159a6a722600777acb555732fb66e /checker | |
| parent | eb842684456c5a965507c83e7b169ae0d0f6cc90 (diff) | |
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
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/cic.mli | 2 | ||||
| -rw-r--r-- | checker/values.ml | 4 |
2 files changed, 4 insertions, 2 deletions
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|]|] |