From 098fb32fe743ac6cc9caa5474c6efd78e1a24de4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Tue, 12 May 2020 18:56:45 +0200 Subject: [PATCH] Remove documentation of -compile, which was removed in #8690. (cherry picked from commit e3e889c01db5382d761d2455370ddc8a793c8e2d) --- doc/sphinx/practical-tools/coq-commands.rst | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index ba43128bdcaf..7856199851e8 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -176,14 +176,8 @@ and ``coqtop``, unless stated otherwise: This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`. :-require *qualid*: Deprecated; use ``-ri`` *qualid*. :-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 ``Qed`` or ``Admitted``), output a ``.vos`` files instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files