diff options
| author | Théo Zimmermann | 2019-11-08 11:22:26 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-08 11:22:26 +0100 |
| commit | c52c1bfef62442d4c318522bddc54a186164b020 (patch) | |
| tree | b2722589f0d520efc62152505d827003a6f6aeca /doc/sphinx/practical-tools | |
| parent | ae7d7e162f3febcad5dd8678f3369cbecccf8f43 (diff) | |
| parent | db391451c5f89c034e6fec1b10fec66a25e3d4d4 (diff) | |
Merge PR #11050: Replace "option" in doc when it refers to a flag
Reviewed-by: Zimmi48
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 |