diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-05-14 09:53:36 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-05-14 09:53:36 +0200 |
| commit | 4ad6855504db2ce15a474bd646e19151aa8142e2 (patch) | |
| tree | b72697c8450705186f1337fe9cc9883106dc458d /toplevel/usage.ml | |
| parent | d91addb140ba7315d70c4599b0d058bef798ac1c (diff) | |
Disable precompilation for native_compute by default.
Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.
Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.
If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.
Failure to precompile is a hard error, since it is now explicitly required
by the user.
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f053839c7..94c1699c2 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) -> |