diff options
| author | Clément Pit-Claudel | 2020-05-12 23:42:43 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-05-12 23:42:43 -0400 |
| commit | 67f0e9fd40dc2f7b30a8aec4c7efb032e61a001e (patch) | |
| tree | a97a373e1fe45a7b7fbd18fd36ca9d495470e4f4 | |
| parent | 4a5944448e31022593df7d6e7e0318cfea92ea98 (diff) | |
| parent | e3e889c01db5382d761d2455370ddc8a793c8e2d (diff) | |
Merge PR #12309: 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 |