diff options
| -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 |