Merge PR #13821: Properly handle ordering of -w and -native-compiler

Reviewed-by: gares

1 files changed, 6 insertions, 1 deletions

diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
index 4dd3f32ad0..9725a849a4 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;