aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-28 01:49:52 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-02 02:26:18 +0100
commit4554a860ffdcb30bf5711bd52f443484f9f950d9 (patch)
tree395170d967938af22d8792ae4e488ad230ad6547 /library
parent0048cbe810c82a775558c14cd7fcae644e205c51 (diff)
[kernel] Patch allowing to disable VM reduction.
The patch has three parts: - Introduction of a configure flag `-bytecode-compiler (yes|no)` (due to static initialization this is a configure-time option) - Installing the hooks that register the VM with the pretyper and the kernel conditionally on the flag. - Replacing the normalization function in `Redexpr` by compute if the VM is disabled. We also rename `Coq_config.no_native_compiler` to `native_compiler` and `Flags.native_compiler` to `output_native_objects` [see #4607].
Diffstat (limited to 'library')
-rw-r--r--library/library.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/library.ml b/library/library.ml
index 88470d121..868e26684 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -170,7 +170,7 @@ let register_loaded_library m =
let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
let f = prefix ^ "cmo" in
let f = Dynlink.adapt_filename f in
- if not Coq_config.no_native_compiler then
+ if Coq_config.native_compiler then
Nativelib.link_library ~prefix ~dirname ~basename:f
in
let rec aux = function
@@ -738,7 +738,7 @@ let save_library_to ?todo dir f otab =
System.marshal_out_segment f' ch (opaque_table : seg_proofs);
close_out ch;
(* Writing native code files *)
- if !Flags.native_compiler then
+ if !Flags.output_native_objects then
let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
if not (Nativelib.compile_library dir ast fn) then
user_err Pp.(str "Could not compile the library to native code.")