diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-02-12 22:33:22 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-02-12 22:34:07 +0100 |
| commit | 7d06e602bea9e7a2c98e1c6badab3a667714b5c8 (patch) | |
| tree | 62409528606ad9df107cf28260f8da8a7fd5b6ba /toplevel/usage.ml | |
| parent | 154bb6a5134c35caea187b83334c098dbadb4e48 (diff) | |
Fix typos about .vio files (thanks Arthur for spotting them)
Diffstat (limited to 'toplevel/usage.ml')
| -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 d4d445699..e9b5e8f84 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -47,6 +47,7 @@ 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\ \n -where print Coq's standard library location and exit\ \n -config print Coq's configuration information and exit\ |