diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 5 | ||||
| -rw-r--r-- | toplevel/usage.ml | 2 |
2 files changed, 5 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 2df7c69c86..0a14a19507 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -498,7 +498,10 @@ let parse_args arglist = |"-noinit"|"-nois" -> load_init := false |"-no-compat-notations" -> no_compat_ntn := true |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true - |"-no-native-compiler" -> no_native_compiler := true + |"-native-compiler" -> + if Coq_config.no_native_compiler then + warning "Native compilation was disabled at configure time." + else native_compiler := true |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true |"-q" -> no_load_rc () diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f053839c70..94c1699c2a 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -71,7 +71,7 @@ let print_usage_channel co command = \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ \n -time display the time taken by each command\ -\n -no-native-compiler disable the native_compute reduction machinery\ +\n -native-compiler precompile files for the native_compute machinery\ \n -h, -help print this list of options\ \n"; List.iter (fun (name, text) -> |