diff options
| author | Jim Fehrle | 2018-08-22 21:43:00 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-09-23 09:32:16 -0700 |
| commit | 02c3cac9fa4f4e88f911486e345740ff7d0a2eab (patch) | |
| tree | dcc40c90d48fbc7d8facc5a9199b326c37d0d895 /doc/tools | |
| parent | 92fbd7383c3897b3932b0ad95afa0982d2d8a7e3 (diff) | |
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 7992c10abb..029e100800 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -558,6 +558,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 |