diff options
| author | Théo Zimmermann | 2019-02-16 15:14:46 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-18 21:24:11 +0100 |
| commit | ea8a9125a4e81e7c848cf53f1e34f534d359e832 (patch) | |
| tree | 3495980fb3efcc41fd2cd658ac3ead6b12f47846 /doc/sphinx/README.rst | |
| parent | 2e4e082637771bc047fbd977aaa5de26956c4618 (diff) | |
[sphinx] Add abort and restart options to directive coqtop.
Diffstat (limited to 'doc/sphinx/README.rst')
| -rw-r--r-- | doc/sphinx/README.rst | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index a341cd9401..accba737fd 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -220,7 +220,7 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo Definition a := 1. The blank line after the directive is required. If you begin a proof, - include an ``Abort`` afterwards to reset coqtop for the next example. + use the ``abort`` option to reset coqtop for the next example. Here is a list of permissible options: @@ -234,7 +234,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo - Behavior options - ``reset``: Send a ``Reset Initial`` command before running this block - - ``fail``: Don't die if a command fails. + - ``fail``: Don't die if a command fails + - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode) + - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any) ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks of the same document (``coqrst`` creates a single ``coqtop`` process per @@ -508,7 +510,7 @@ Tips and tricks Nested lemmas ------------- -The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas:: +The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas (which by default results in a failure):: .. coqtop:: all @@ -518,7 +520,7 @@ The ``.. coqtop::`` directive does *not* reset Coq after running its contents. Lemma l2: 2 + 2 <> 1. -Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas. +Add either ``abort`` to the first block or ``reset`` to the second block to avoid nesting lemmas. Abbreviations and macros ------------------------ |