aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativeconv.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-05 14:25:10 +0100
committerPierre-Marie Pédrot2018-11-05 14:25:10 +0100
commitea678521c9eda7acde3a0276e0cec0931dbc6416 (patch)
treecbc2baf5777992a7e81e24a662dfce5db311d6a2 /kernel/nativeconv.ml
parentafc3e334c02cbbbe395387ff7110a296dce6c9f6 (diff)
parente2e7fea91f3af5dcf62052078da65489b796e9e2 (diff)
Merge PR #8870: Pass native and VM flags to the kernel through environment
Diffstat (limited to 'kernel/nativeconv.ml')
-rw-r--r--kernel/nativeconv.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 054b6a2d17..f5d7ab3c9d 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -14,7 +14,8 @@ open Nativelib
open Reduction
open Util
open Nativevalues
-open Nativecode
+open Nativecode
+open Environ
(** This module implements the conversion test by compiling to OCaml code *)
@@ -142,7 +143,7 @@ let warn_no_native_compiler =
strbrk " falling back to VM conversion test.")
let native_conv_gen pb sigma env univs t1 t2 =
- if not Coq_config.native_compiler then begin
+ if not (typing_flags env).Declarations.enable_native_compiler then begin
warn_no_native_compiler ();
Vconv.vm_conv_gen pb env univs t1 t2
end