5 files changed, 23 insertions, 17 deletions

diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index c4f12f6bb7..1738d56a54 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -44,6 +44,7 @@ type option_command =
 type injection_command =
   | OptionInjection of (Goptions.option_name * option_command)
   | RequireInjection of (string * string option * bool option)
+  | WarnNoNative of string
 
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
@@ -255,12 +256,6 @@ let parse_option_set opt =
     let v = String.sub opt (eqi+1) (len - eqi - 1) in
     to_opt_key (String.sub opt 0 eqi), Some v
 
-let warn_no_native_compiler =
-  CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
-    Pp.(fun s -> strbrk "Native compiler is disabled," ++
-                   strbrk " -native-compiler " ++ strbrk s ++
-                   strbrk " option ignored.")
-
 let get_native_compiler s =
   (* We use two boolean flags because the four states make sense, even if
   only three are accessible to the user at the moment. The selection of the
@@ -274,10 +269,8 @@ let get_native_compiler s =
     | _ ->
        error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in
   if Coq_config.native_compiler = NativeOff && n <> NativeOff then
-    let () = warn_no_native_compiler s in
-    NativeOff
-  else
-    n
+    NativeOff, Some (WarnNoNative s)
+  else n, None
 
 (* Main parsing routine *)
 (*s Parsing of the command line *)
@@ -385,8 +378,9 @@ let parse_args ~usage ~init arglist : t * string list =
       { oval with config = { oval.config with enable_VM = get_bool ~opt (next ()) }}
 
     |"-native-compiler" ->
-      let native_compiler = get_native_compiler (next ()) in
-      { oval with config = { oval.config with native_compiler }}
+      let native_compiler, warn = get_native_compiler (next ()) in
+      { oval with config = { oval.config with native_compiler };
+                  pre = { oval.pre with injections = Option.List.cons warn oval.pre.injections }}
 
     | "-set" ->
       let opt, v = parse_option_set @@ next() in
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
index aef50193f2..ce0a0cdf16 100644
--- a/sysinit/coqargs.mli
+++ b/sysinit/coqargs.mli
@@ -28,7 +28,12 @@ type injection_command =
      ready. Parameters follow [Library], that is to say,
      [lib,prefix,import_export] means require library [lib] from
      optional [prefix] and [import_export] if [Some false/Some true]
-     is used.  *)
+      is used.  *)
+  | WarnNoNative of string
+  (** Used so that "-w -native-compiler-disabled -native-compiler yes"
+     does not cause a warning. The native option must be processed
+     before injections (because it affects require), so the
+     instruction to emit a message is separated. *)
 
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml
index 16c8389de5..25da2c5302 100644
--- a/sysinit/coqinit.ml
+++ b/sysinit/coqinit.ml
@@ -126,10 +126,16 @@ let require_file (dir, from, exp) =
   let mfrom = Option.map Libnames.qualid_of_string from in
   Flags.silently (Vernacentries.vernac_require mfrom exp) [mp]
 
-let handle_injection = function
-  | Coqargs.RequireInjection r -> require_file r
-  (* | LoadInjection l -> *)
-  | Coqargs.OptionInjection o -> Coqargs.set_option o
+let warn_no_native_compiler =
+  CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
+    Pp.(fun s -> strbrk "Native compiler is disabled," ++
+                   strbrk " -native-compiler " ++ strbrk s ++
+                   strbrk " option ignored.")
+
+let handle_injection = let open Coqargs in function
+  | RequireInjection r -> require_file r
+  | OptionInjection o -> set_option o
+  | WarnNoNative s -> warn_no_native_compiler s
 
 let start_library ~top injections =
   Flags.verbosely Declaremods.start_library top;
diff --git a/test-suite/output/bug_13821_native_command_line_warn.out b/test-suite/output/bug_13821_native_command_line_warn.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/bug_13821_native_command_line_warn.out
diff --git a/test-suite/output/bug_13821_native_command_line_warn.v b/test-suite/output/bug_13821_native_command_line_warn.v
new file mode 100644
index 0000000000..a28210b6c2
--- /dev/null
+++ b/test-suite/output/bug_13821_native_command_line_warn.v
@@ -0,0 +1 @@
+(* -*- coq-prog-args: ("-w" "-native-compiler-disabled" "-native-compiler" "ondemand"); -*- *)