diff options
| author | Jim Fehrle | 2018-09-01 12:39:09 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-09-20 18:27:08 -0700 |
| commit | ec7dd674ea25dfd36c007bb863fed63ce8d31ff2 (patch) | |
| tree | 2f73dd477ac9276ba8ed9409aab613370d29c7fb /doc/sphinx/addendum/parallel-proof-processing.rst | |
| parent | d4b5de427d94d82f09d58e0f1095f052a5900914 (diff) | |
Rewrite "Flags, Options and Tables" section.
Mark boolean-valued options with :flag:
Adjust tactic and command names so parameters aren't shown in the index unless
they're needed for disambiguation.
Remove references to synchronous options.
Revise doc for tables.
Correct indentation for text below :flag:
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. |