diff options
| author | Théo Zimmermann | 2020-05-12 18:56:45 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-12 18:56:45 +0200 |
| commit | e3e889c01db5382d761d2455370ddc8a793c8e2d (patch) | |
| tree | 994235573bde2cc5bd1f17e2fc94dbe15bd0ace9 | |
| parent | 007ed9e21f69a157ffff3fa5f990f62ab2756416 (diff) | |
Remove documentation of -compile, which was removed in #8690.
| -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 545bba4930..58fd49c390 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -175,14 +175,8 @@ and ``coqtop``, unless stated otherwise: :-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@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 |