Properly disable native compilation when -native-compiler is unset.

There was a function used by the pretyper that did not check that the flag was
set, leading to native compilation even when the configure flag was off.

1 files changed, 11 insertions, 11 deletions

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index e97dbd0d67..931b8bbc86 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -135,7 +135,18 @@ and conv_fix env lvl t1 f1 t2 f2 cu =
     else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in
   aux 0 cu
 
+let warn_no_native_compiler =
+  let open Pp in
+  CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
+         (fun () -> strbrk "Native compiler is disabled," ++
+                      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
+    warn_no_native_compiler ();
+    Vconv.vm_conv_gen pb env univs t1 t2
+  end
+  else
   let ml_filename, prefix = get_ml_filename () in
   let code, upds = mk_conv_code env sigma prefix t1 t2 in
   match compile ml_filename code ~profile:false with
@@ -152,19 +163,8 @@ let native_conv_gen pb sigma env univs t1 t2 =
       end
   | _ -> anomaly (Pp.str "Compilation failure.") 
 
-let warn_no_native_compiler =
-  let open Pp in
-  CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
-         (fun () -> strbrk "Native compiler is disabled," ++
-                      strbrk " falling back to VM conversion test.")
-
 (* Wrapper for [native_conv] above *)
 let native_conv cv_pb sigma env t1 t2 =
-  if not Coq_config.native_compiler then begin
-    warn_no_native_compiler ();
-    Vconv.vm_conv cv_pb env t1 t2
-  end
-  else
   let univs = Environ.universes env in
   let b =
     if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2