- flushed proof-done-advancing-require-function and

  proof-shell-require-command-regexp
- TAGS updated to really flush them

1 files changed, 1 insertions, 14 deletions

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index c526d2df..27dcb0df 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -1918,22 +1918,9 @@ be set non-nil, so that when a completed file is activated for
 scripting (to do undo operations), the whole history is discarded.
 @end defvar
 
-@c TEXI DOCSTRING MAGIC: proof-shell-require-command-regexp
-@defvar proof-shell-require-command-regexp 
-A regular expression to match a Require-type of command, or nil.@*
-If set to a regexp, then @samp{@code{proof-done-advancing-require-function}}
-should also be set, and will be called immediately after the match.
 
-This can be used to adjust @samp{@code{proof-included-files-list}} based on the
-lines of script that have been processed/parsed, rather than relying
-on information from the prover.
-@end defvar
 
-@c TEXI DOCSTRING MAGIC: proof-done-advancing-require-function
-@defvar proof-done-advancing-require-function 
-Used in @samp{@code{proof-done-advancing}}, see @samp{@code{proof-shell-require-command-regexp}}.@*
-The function is passed the span and the command as arguments.
-@end defvar
+
 @node Hooks and other settings
 @section Hooks and other settings