diff options
Diffstat (limited to 'sysinit/coqinit.ml')
| -rw-r--r-- | sysinit/coqinit.ml | 14 |
1 files changed, 10 insertions, 4 deletions
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; |