diff options
| author | Gaëtan Gilbert | 2021-02-04 12:14:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-02-04 12:21:12 +0100 |
| commit | 74aabc032014b0b83f2d54996dbb76cb5a78ea4d (patch) | |
| tree | 639390a8829b8a3a91ec6361e049db1ad69f46db /sysinit/coqargs.mli | |
| parent | 4b7feb4e022eab13ead7468687a53bc5afae0f8f (diff) | |
Properly handle ordering of -w and -native-compiler
Warnings are handled as injection commands, interleaved with options
and requires. Native compiler impacts require, so we must convert
"yes" to "no" before handling injections. As such the semantic
handling of the native command line argument must be separated from
the emission of the warning message, which this PR implements.
Fix #13819
In principle the other 2 cwarning in coqargs
(deprecated spropcumul and inputstate) should be moved to injections
too, but since they're deprecated I can't be bothered.
Diffstat (limited to 'sysinit/coqargs.mli')
| -rw-r--r-- | sysinit/coqargs.mli | 7 |
1 files changed, 6 insertions, 1 deletions
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; |