From 02c3cac9fa4f4e88f911486e345740ff7d0a2eab Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 22 Aug 2018 21:43:00 -0700
Subject: Documentation for proof diffs

---
 doc/tools/coqrst/coqdomain.py | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'doc/tools')

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
-- 
cgit v1.2.3