- fixed compilation errors

3 files changed, 22 insertions, 4 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 0a8ec0ed..09d1a484 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -15,6 +15,7 @@
 
 (eval-when (compile)
   (require 'proof-utils)
+  (require 'proof-shell)
   (require 'span)
   (require 'outline)
   (require 'newcomment)
@@ -830,7 +831,7 @@ This is specific to `coq-mode'."
   (setq proof-cannot-reopen-processed-files nil
         proof-auto-multiple-files t
         ;; proof-shell-inform-file-retracted-cmd 'coq-retract-file
-        proof-shell-require-command-regexp coq-require-command-regexp
+        ;; proof-shell-require-command-regexp coq-require-command-regexp
         proof-done-advancing-require-function 'coq-process-require-command)
 
   (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t)
@@ -1554,6 +1555,12 @@ queue."
         (coq-make-lib-up-to-date (symbol-value coq-object-local-hash-symbol)
                                  module-obj-file)))))
 
+(defvar coq-process-require-current-buffer
+  "Used in `coq-compile-save-some-buffers' and `coq-compile-save-buffer-filter'.
+This only locally used variable communicates the current buffer
+from `coq-compile-save-some-buffers' to
+`coq-compile-save-buffer-filter'.")
+
 (defun coq-compile-save-buffer-filter ()
   "Filter predicate for `coq-compile-save-some-buffers'.
 See also `save-some-buffers'. Returns t for buffers with major mode
diff --git a/generic/proof-config.el b/generic/proof-config.el
index cf090aa1..cb24657f 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1552,9 +1552,11 @@ if you don't need it (slight speed penalty)."
 
 (defcustom proof-shell-extend-queue-hook nil
   "Hooks run by proof-extend-queue before extending `proof-action-list'.
-Can be used to run additional actions before items are added to the queue
-\(such as recompiling required modules for Coq) or to modify the items
-that are going to be added to `proof-action-list'."
+Can be used to run additional actions before items are added to
+the queue \(such as compiling required modules for Coq) or to
+modify the items that are going to be added to
+`proof-action-list'. The items that are about to be added are
+bound to `queueitems'."
   :type '(repeat function)
   :group 'proof-shell)  
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index f5825516..dcd36a6c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -922,6 +922,15 @@ This function calls `proof-add-to-queue'."
       (proof-set-queue-endpoints start end))
   (proof-add-to-queue queueitems queuemode))
 
+
+(defvar queueitems
+  "Local variable of `proof-extend-queue' and `proof-shell-extend-queue-hook'.
+This only locally used variable communicates the items that are
+about to be placed into the `proof-action-list' queue into the
+hook functions in `proof-shell-extend-queue-hook'. This is the
+price to pay for using a normal hook.")
+
+
 ;;;###autoload
 (defun proof-extend-queue (end queueitems)
   "Extend the current queue with QUEUEITEMS, queue end END.