diff options
| author | Théo Zimmermann | 2018-10-01 11:54:22 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-01 11:54:22 +0200 |
| commit | 9134d94d42bafd38dfcc6a09a99edd554e636b55 (patch) | |
| tree | f945ea81de26d9748e833762b87789f62e77ea5f /doc/tools | |
| parent | cce3f57a9f0299e9010ea5af666f8e9e7055fc34 (diff) | |
| parent | 02c3cac9fa4f4e88f911486e345740ff7d0a2eab (diff) | |
Merge PR #8301: Documentation for proof diffs
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index edf4e6ec9d..2c69dcfe08 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -560,6 +560,9 @@ class CoqtopDirective(Directive): Print nat. 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. + Here is a list of permissible options: - Display options |