aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2001-09-09 14:06:44 +0000
committerDavid Aspinall2001-09-09 14:06:44 +0000
commit16b07908a5e7f75dd29043e39b9127007e67dcff (patch)
treed9024d4d4b332f06d7ffc6e01a08495cae34dcb5
parent873f7a1ecd32f08e72f6aa551bc0faa69ac5dcc2 (diff)
Update docs.
-rw-r--r--doc/PG-adapting.texi5
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index af0984bb..faf12742 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -859,8 +859,8 @@ Regexp which matches a command to save a named theorem.@*
The name of the theorem is build from the variable
@code{proof-save-with-hole-result} using the same convention as
@code{query-replace-regexp}.
-Used for setting names of goal..save regions and for default
-@code{function-menu} configuration in @code{proof-script-find-next-entity}.
+Used for setting names of goal..save and proof regions and for
+default @code{function-menu} configuration in @code{proof-script-find-next-entity}.
It's safe to leave this setting as nil.
@end defvar
@@ -2720,6 +2720,7 @@ important one is @code{proof-init-segmentation}.
Initialise the queue and locked spans in a proof script buffer.@*
Allocate spans if need be. The spans are detached from the
buffer, so the regions are made empty by this function.
+Also clear list of script portions.
@end defun
For locking files loaded by a proof assistant, we use the next function.