From 4554a860ffdcb30bf5711bd52f443484f9f950d9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 28 Nov 2017 01:49:52 +0100
Subject: [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].
---
 pretyping/nativenorm.ml | 4 ++--
 pretyping/vnorm.ml      | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index dafe8cb269..79e0afa72b 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -436,11 +436,11 @@ let stop_profiler m_pid =
   match profiler_platform() with
     "Unix (Linux)" -> stop_profiler_linux m_pid
   | _ -> ()
-     
+
 let native_norm env sigma c ty =
   let c = EConstr.Unsafe.to_constr c in
   let ty = EConstr.Unsafe.to_constr ty in
-  if Coq_config.no_native_compiler then
+  if not Coq_config.native_compiler then
     user_err Pp.(str "Native_compute reduction has been disabled at configure time.")
   else
   let penv = Environ.pre_env env in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b5b8987e33..e395bdbc63 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -365,4 +365,4 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
   Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb)
     ~catch_incon:true ~pb env sigma t1 t2
 
-let _ = Reductionops.set_vm_infer_conv vm_infer_conv
+let _ = if Coq_config.bytecode_compiler then Reductionops.set_vm_infer_conv vm_infer_conv
-- 
cgit v1.2.3