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

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

2 files changed, 2 insertions, 30 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index b5289234..92b24db1 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -992,23 +992,6 @@ scripting (to do undo operations), the whole history is discarded."
   :type 'boolean
   :group 'proof-shell)  ;; not really proof shell
 
-(defcustom proof-shell-require-command-regexp nil
-  "A regular expression to match a Require-type of command, or nil.
-If set to a regexp, then `proof-done-advancing-require-function'
-should also be set, and will be called immediately after the match.
-
-This can be used to adjust `proof-included-files-list' based on the
-lines of script that have been processed/parsed, rather than relying
-on information from the prover."
-  :type 'regexp
-  :group 'proof-shell)
-
-(defcustom proof-done-advancing-require-function nil
-  "Used in `proof-done-advancing', see `proof-shell-require-command-regexp'.
-The function is passed the span and the command as arguments."
-  :type 'function
-  :group 'proof-shell)
-
 ;; (defcustom  proof-shell-adjust-line-width-cmd nil
 
 ;;
diff --git a/generic/proof-script.el b/generic/proof-script.el
index a7ed146e..ce98409b 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1365,19 +1365,8 @@ Argument SPAN has just been processed."
       (proof-done-advancing-autosave span))
 
      ;; CASE 4: A "Require" type of command is seen (Coq).
-     ;;
-     ((and
-       proof-shell-require-command-regexp
-       (proof-string-match proof-shell-require-command-regexp cmd))
-      ;; We take additional action dependent on prover
-      ;; [FIXME: use same method as in proof-shell here to
-      ;;  recompute proof-included-files and adjust it]
-      ;; FIXME 2: we could annotate the Require ourselves
-      ;; at this point to contain the buffers which are
-      ;; being included!  Then undoing can retract them.
-      (funcall proof-done-advancing-require-function span cmd)
-      ;; But do what we would have done anyway
-      (proof-done-advancing-other span))
+     ;; Case 4 has been flushed, because its functionality has been
+     ;; superseeded by the new auto-compilation feature for Coq.
 
      ;; CASE 5:  Some other kind of command (or a nested goal).
      (t