diff options
| author |  Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-04-29 23:55:51 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-05-15 12:05:44 -0400 |
| commit | 6f3a8a90514669c84be4de5726fe65f15141ca4d (patch) | |
| tree | 63a3e351d237a3aa020bd653292fd0778a996762 /doc/tools/coqrst/coqdomain.py | |
| parent | efa6ef592e29bb4bc862a114c399d660580bba66 (diff) | |
[doc] Add a README to doc/sphinx/
The readme is auto-generated by combining introductory text with the docstrings
in coqdomain.py.
Diffstat (limited to 'doc/tools/coqrst/coqdomain.py')
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 75ed70e08..3cad394e6 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -433,12 +433,15 @@ class CoqtopDirective(Directive): Here is a list of permissible options: - Display + - Display options + - ``all``: Display input and output - ``in``: Display only input - ``out``: Display only output - ``none``: Display neither (useful for setup commands) - Behaviour + + - 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 |