diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 2 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
3 files changed, 3 insertions, 2 deletions
@@ -292,7 +292,7 @@ Tools added to the load path. (Same behavior as with coq/user-contrib.) - coqdep accepts a -dumpgraph option generating a dot file. - Makefiles generated through coq_makefile have three new targets "quick" - "checkproof" and "vio2vo", allowing respectively to asynchronously compile + "checkproofs" and "vio2vo", allowing respectively to asynchronously compile the files without playing the proof scripts, asynchronously checking that the quickly generated proofs are correct and generating the object files from the quickly generated proofs. diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 71eb0108d3..11b4f26145 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1059,7 +1059,7 @@ Please note that the questions described here have been subject to redesign in Coq v8.5. Former versions of Coq use the same terminology to describe slightly different things. -Compiled files (\texttt{.vo} and \texttt{.vi}) store sub-libraries. In +Compiled files (\texttt{.vo} and \texttt{.vio}) store sub-libraries. In order to refer to them inside {\Coq}, a translation from file-system names to {\Coq} names is needed. In this translation, names in the file system are called {\em physical} paths while {\Coq} names are diff --git a/toplevel/usage.ml b/toplevel/usage.ml index d4d4456994..e9b5e8f84a 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\ |