diff options
| author | Jim Fehrle | 2019-11-04 19:14:07 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2019-11-06 11:24:27 -0800 |
| commit | db391451c5f89c034e6fec1b10fec66a25e3d4d4 (patch) | |
| tree | 49187070f11a607d08e2dad51da14cc823b863ef /doc/sphinx/practical-tools | |
| parent | 634cb7b8a07a34fc29d074591091f0a6170f7bff (diff) | |
Replace "option" in doc when it refers to a flag
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 70259ff565..97e7af8cb4 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -36,7 +36,7 @@ toplevel with the command ``Coqloop.loop();;``. .. flag:: Coqtop Exit On Error - This option, off by default, causes coqtop to exit with status code + This flag, off by default, causes coqtop to exit with status code ``1`` if a command produces an error instead of recovering from it. Batch compilation (coqc) @@ -219,7 +219,7 @@ and ``coqtop``, unless stated otherwise: .. warning:: This makes the logic inconsistent. :-mangle-names *ident*: *Experimental.* Do not depend on this option. Replace Coq's auto-generated name scheme with names of the form *ident0*, *ident1*, - etc. Within Coq, the flag :flag:`Mangle Names` turns this behavior on, + etc. Within Coq, the :flag:`Mangle Names` flag turns this behavior on, and the :opt:`Mangle Names Prefix` option sets the prefix to use. This feature is intended to be used as a linter for developments that want to be robust to changes in the auto-generated name scheme. The options are provided to |