diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-03-25 11:09:56 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-03-25 11:10:00 +0100 |
| commit | 57109109a53c4bbbd7c8fa0acc142e47c80c5df7 (patch) | |
| tree | 3e60ca8fd3fbaefedb4dec1b26ab74948967a220 /toplevel/usage.ml | |
| parent | f54d0b3158bc69a11fe579289f06f164ff5ccb94 (diff) | |
coqc: fix --help
Diffstat (limited to 'toplevel/usage.ml')
| -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 6909d8944..4ee3bc474 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\ |