diff options
| -rw-r--r-- | toplevel/usage.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 6909d89440..4ee3bc4745 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -48,6 +48,10 @@ let print_usage_channel co command = \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\ |