diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index ca167c8b4b..d4ceffac9f 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -202,14 +202,8 @@ and ``coqtop``, unless stated otherwise: See the :ref:`note above <interleave-command-line>` regarding the order of command-line options. :-batch: Exit just after argument parsing. Available for ``coqtop`` only. -:-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option - implies -batch (exit just after argument parsing). It is available only - for `coqtop`, as this behavior is the purpose of ``coqc``. -:-compile-verbose *file.v*: Deprecated. Use ``coqc -verbose``. Same as -compile but also output the - content of *file.v* as it is compiled. :-verbose: Output the content of the input file as it is compiled. - This option is available for ``coqc`` only; it is the counterpart of - -compile-verbose. + This option is available for ``coqc`` only. :-vos: Indicate |Coq| to skip the processing of opaque proofs (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files |