diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-01-12 15:38:40 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-01-12 15:38:40 +0100 |
| commit | 13a55aa2e8fd999a96cf1e4df5a0e34f26e3dcc8 (patch) | |
| tree | 3b642bb9c8678dda1a6e4154c6dd59b143a6bb6b | |
| parent | 940674b4c696b82ad7e5f0efd71c2de7de3d6301 (diff) | |
Add -no-native-compiler flag to list dumped by --help.
| -rw-r--r-- | toplevel/usage.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 8b5481979..d4d445699 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -67,6 +67,7 @@ let print_usage_channel co command = \n -impredicative-set set sort Set impredicative\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -time display the time taken by each command\ +\n -no-native-compiler disable the native_compute reduction machinery\ \n -h, -help print this list of options\ \n"; List.iter (fun (name, text) -> |