diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-08-07 13:59:14 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-07 13:59:14 +0000 |
| commit | 51c2131c3f17accb377a336aba18ecdfa4b13fc1 (patch) | |
| tree | df1bc8cdc7dbd3b52316093d05cb13594f15df7e /generic | |
| parent | 35dae9b203b0fc918e56deb9926b44d19042ed9d (diff) | |
Fix docs
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 6 |
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 |