diff options
| author | Théo Zimmermann | 2018-09-21 14:10:51 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-21 14:10:51 +0200 |
| commit | 63e21181b92e61616f749b4554bb761bee5fa8ac (patch) | |
| tree | b74d7d19034ef835ae04566f31ae4b03a6a04c4a /doc/sphinx/addendum/parallel-proof-processing.rst | |
| parent | bceb3bc784d5ce196e06815bd91963607a35a62c (diff) | |
| parent | ec7dd674ea25dfd36c007bb863fed63ce8d31ff2 (diff) | |
Merge PR #8439: Update documentation of options and flags
Diffstat (limited to 'doc/sphinx/addendum/parallel-proof-processing.rst')
| -rw-r--r-- | doc/sphinx/addendum/parallel-proof-processing.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index eb19d57203..8b7214e2ab 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -58,7 +58,7 @@ variables used. Automatic suggestion of proof annotations ````````````````````````````````````````` -The command ``Set Suggest Proof Using`` makes |Coq| suggest, when a ``Qed`` +The flag :flag:`Suggest Proof Using` makes |Coq| suggest, when a ``Qed`` command is processed, a correct proof annotation. It is up to the user to modify the proof script accordingly. |