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.

1 files changed, 4 insertions, 3 deletions

diff --git a/vernac/library.ml b/vernac/library.ml
index 244424de6b..6ed38410c4 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -159,11 +159,12 @@ 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 Coq_config.native_compiler then
-      Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f
+    Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f
   in
   let rec aux = function
-    | [] -> link (); [libname]
+    | [] ->
+      let () = if Flags.get_native_compiler () then link () in
+      [libname]
     | m'::_ as l when DirPath.equal m' libname -> l
     | m'::l' -> m' :: aux l' in
   libraries_loaded_list := aux !libraries_loaded_list;