diff options
| author | Gaëtan Gilbert | 2019-02-12 14:39:43 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-12 14:39:43 +0100 |
| commit | 912e363c9152012ecbff5272cded46e75a2f3c33 (patch) | |
| tree | db8a6fdd6554e115e15501e98808f8b7196eb332 /doc/tools | |
| parent | f1e54f2521bba13c59e89b4c06f2811866b5f92d (diff) | |
Fix doc for coqtop:: undo
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 |