aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-07 13:59:14 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-07 13:59:14 +0000
commit51c2131c3f17accb377a336aba18ecdfa4b13fc1 (patch)
treedf1bc8cdc7dbd3b52316093d05cb13594f15df7e /generic
parent35dae9b203b0fc918e56deb9926b44d19042ed9d (diff)
Fix docs
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-config.el6
1 files changed, 4 insertions, 2 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 2411f19a..1a8d2b65 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -2217,8 +2217,10 @@ See `pg-subterm-start-char'."
"Annotation character that indicates the beginning of a \"top\" element.
A \"top\" element may be a sub-goal to be proved or a named hypothesis,
for example. It is currently assumed (following LEGO/Coq conventions)
-to span a whole line (the region marked in .
-The function `pg-topterm-goalhyp-fn' examines text following
+to span a whole line.
+
+The function `pg-topterm-goalhyp-fn' examines text following this
+special character, to determine what kind of top element it is.
This setting is also used to see if proof-by-pointing features
are configured. If it is unset, some of the code