coqargs: use algebraic datatype for -native-compiler

1 files changed, 3 insertions, 2 deletions

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 31656e0b07..3fe6ad0718 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -96,6 +96,9 @@ let compile opts copts ~echo ~f_in ~f_out =
   let iload_path = build_load_path opts in
   let require_libs = require_libs opts in
   let stm_options = opts.stm_flags in
+  let output_native_objects = match opts.native_compiler with
+    | NativeOff -> false | NativeOn {ondemand} -> not ondemand
+  in
   match copts.compilation_mode with
   | BuildVo ->
       Flags.record_aux_file := true;
@@ -125,7 +128,6 @@ let compile opts copts ~echo ~f_in ~f_out =
       let _doc = Stm.join ~doc:state.doc in
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
-      let output_native_objects = opts.output_native_objects in
       Library.save_library_to ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ());
       Aux_file.record_in_aux_at "vo_compile_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
@@ -169,7 +171,6 @@ let compile opts copts ~echo ~f_in ~f_out =
       let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in
       let doc = Stm.finish ~doc:state.doc in
       check_pending_proofs ();
-      let output_native_objects = opts.output_native_objects in
       let () = ignore (Stm.snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vio) in
       Stm.reset_task_queue ()