diff options
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index d4d44569..f053839c 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -23,9 +23,7 @@ let print_usage_channel co command = output_string co " -I dir look for ML files in dir\ \n -include dir (idem)\ -\n -I dir -as coqdir implicitly map physical dir to logical coqdir\ -\n -R dir -as coqdir recursively map physical dir to logical coqdir\ -\n -R dir coqdir (idem)\ +\n -R dir coqdir recursively map physical dir to logical coqdir\ \n -Q dir coqdir map physical dir to logical coqdir\ \n -top coqdir set the toplevel name to be coqdir instead of Top\ \n -notop set the toplevel name to be the empty logical path\ @@ -47,6 +45,11 @@ let print_usage_channel co command = \n -require f load Coq object file f.vo and import it (Require f.)\ \n -compile f compile Coq file f.v (implies -batch)\ \n -compile-verbose f verbosely compile Coq file f.v (implies -batch)\ +\n -quick quickly compile .v files to .vio files (skip proofs)\ +\n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\ +\n into fi.vo\ +\n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\ +\n proofs in each fi.vio\ \n\ \n -where print Coq's standard library location and exit\ \n -config print Coq's configuration information and exit\ @@ -66,6 +69,7 @@ let print_usage_channel co command = \n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\ \n -impredicative-set set sort Set impredicative\ \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 -h, -help print this list of options\ |