diff options
| author | Théo Zimmermann | 2019-02-13 11:49:29 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-13 11:49:29 +0100 |
| commit | 90e2fa3344cff478a2ab23c0dbbb5eab5b4668e4 (patch) | |
| tree | 7ad437364d4998e8a95ee8c0d1a1827099bd8084 /doc/tools | |
| parent | 0b0fa735dc0da5660a870053a5a5f6fd1c5e22d1 (diff) | |
| parent | d638148dc3e0220ac99761cf9f2efa8284882c41 (diff) | |
Merge PR #9553: Sphinx various fixing of failing commands
Ack-by: Zimmi48
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 067af954ad..0dd9b3aa3e 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -560,7 +560,7 @@ class CoqtopDirective(Directive): Example:: - .. coqtop:: in reset undo + .. coqtop:: in undo Print nat. Definition a := 1. @@ -580,8 +580,7 @@ class CoqtopDirective(Directive): - Behavior options - ``reset``: Send a ``Reset Initial`` command before running this block - - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after - running all the commands in this block + - ``undo``: Reset state after executing. Not compatible with ``reset``. ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks of the same document (``coqrst`` creates a single ``coqtop`` process per |