From acba2419a4cebb2b55bad2aefa2062640ffe8828 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 18 Dec 2019 15:55:23 +0100
Subject: Centralize the flag handling native compilation.

Instead of relying on the Coq_config immutable flag, we introduce an
initialization-only flag to govern the use of the native compiler. This
allows to make coqc passed with "-native-compiler no" behave as if it had
been configured without native compilation.
---
 pretyping/nativenorm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 2db674d397..f87a350728 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -486,8 +486,8 @@ let stop_profiler 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 not Coq_config.native_compiler then
-    user_err Pp.(str "Native_compute reduction has been disabled at configure time.")
+  if not (Flags.get_native_compiler ()) then
+    user_err Pp.(str "Native_compute reduction has been disabled.")
   else
   (*
   Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
-- 
cgit v1.2.3