Attempt to support stricter bytecomp flags

4 files changed, 31 insertions, 28 deletions

diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index bd57ae0f..82c3f93e 100644
--- a/coq/coq-local-vars.el
+++ b/coq/coq-local-vars.el
@@ -11,7 +11,9 @@
 
 (require 'local-vars-list)              ; in lib directory
 
-(require 'cl)
+(eval-when-compile
+  (require 'cl))
+
 (eval-when (compile)
   (defvar coq-prog-name nil)
   (defvar coq-load-path nil))
diff --git a/coq/coq.el b/coq/coq.el
index f3f0b230..a67954ca 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -3,15 +3,14 @@
 ;; Authors: Healfdene Goguen, Pierre Courtieu
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
-
+;;
 ;; $Id$
 
 
-;;; Commentary:
-;;
-;;; History:
 
-(require 'cl)
+(eval-when-compile
+  (require 'cl)
+  (require 'proof-compat))
 
 (eval-when (compile)
   (require 'proof-utils)
@@ -22,8 +21,7 @@
   (require 'etags)
   (unless (proof-try-require 'smie)
     (defvar smie-indent-basic nil)
-    (defvar smie-rules-function nil))     ; smie
-
+    (defvar smie-rules-function nil))
   (defvar queueitems nil)       ; dynamic scope in p-s-extend-queue-hook
   (defvar coq-time-commands nil)        ; defpacustom
   (defvar coq-use-editing-holes nil)    ; defpacustom
@@ -31,8 +29,14 @@
   (defvar coq-confirm-external-compilation nil) ; defpacustom
   (proof-ready-for-assistant 'coq))     ; compile for coq
 
+(require 'proof)
+(require 'pg-custom)                    ; declares coq-prog-args
+(require 'coq-syntax)                   ; sets coq-prog-name
+(require 'coq-local-vars)               ;
+(require 'coq-abbrev)                   ; coq specific menu
+
 
-;; FIXME: making these declarations conditional doesn't work
+;; for compilation in Emacs < 23.3 (NB: declare function only works at top level)
 (declare-function smie-bnf->prec2 "smie")
 (declare-function smie-rule-parent-p "smie")
 (declare-function smie-default-forward-token "smie")
@@ -41,10 +45,7 @@
 (declare-function smie-rule-separator "smie")
 (declare-function smie-rule-parent "smie")
 
-(require 'proof)
-(require 'coq-syntax)                   ; sets coq-prog-name
-(require 'coq-local-vars)               ;
-(require 'coq-abbrev)                   ; coq specific menu
+(declare-function some "cl-extra")      ; spurious bytecomp warning
 
 
 
@@ -68,7 +69,7 @@ See also `coq-prog-env' to adjust the environment."
    :group 'coq)
 
 ;; coq-prog-args is the user-set list of arguments to pass to Coq process,
-;; see 'defpacustom prog-args' in proof-config for documentation.
+;; see 'defpacustom prog-args' in pg-custom.el for documentation.
 
 ;; For Coq, this should contain -emacs.
 ;; -translate will be added automatically to this list if `coq-translate-to-v8'
@@ -79,15 +80,14 @@ See also `coq-prog-env' to adjust the environment."
   :type 'boolean
   :group 'coq)
 
-;; Fixes default prog args, this is overridden by file variables
 (defun coq-build-prog-args ()
-  (setq coq-prog-args
-        (append (remove-if (lambda (x) (string-match "-emacs" x)) coq-prog-args)
-                '("-emacs-U")
-                (if coq-translate-to-v8 " -translate"))))
+  "Adjusts default `coq-prog-args'.  May be overridden by file variables."
+  (delete "-emacs" coq-prog-args)
+  (add-to-list 'coq-prog-args "-emacs-U")
+  (if coq-translate-to-v8 
+      (add-to-list 'coq-prog-args "-translate")))
 
-;; fix it
-(unless noninteractive ;; compiling
+(unless noninteractive   ;; compiling
   (coq-build-prog-args))
 
 (defcustom coq-compiler
@@ -1512,8 +1512,8 @@ is up-to-date."
         (message "Ignore lib file %s" lib-obj-file))
     t)
    (if (some
-        (lambda (dir-regexp) (string-match dir-regexp lib-obj-file))
-        coq-compile-ignored-directories)
+          (lambda (dir-regexp) (string-match dir-regexp lib-obj-file))
+          coq-compile-ignored-directories)
        (progn
          (if coq-debug-auto-compilation
              (message "Ignore %s" lib-obj-file))
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index b188d978..cd9dac2a 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -33,6 +33,7 @@
 (declare-function pg-response-warning "pg-response")
 (declare-function pg-response-message "pg-response")
 (declare-function proof-segment-up-to "proof-script") 
+(declare-function proof-insert-pbp-command "proof-script")
 
 ;;; Code:
 (defalias 'pg-pgip-debug   'proof-debug)
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 0f8e1585..d0f8db5a 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -209,7 +209,7 @@ Initialise the goals buffer after the child has been configured.
 ;;;***
 
 ;;;### (autoloads (pg-movie-export-directory pg-movie-export-from
-;;;;;;  pg-movie-export) "pg-movie" "pg-movie.el" (20123 64083))
+;;;;;;  pg-movie-export) "pg-movie" "pg-movie.el" (20123 64158))
 ;;; Generated autoloads from pg-movie.el
 
 (autoload 'pg-movie-export "pg-movie" "\
@@ -281,7 +281,7 @@ This macro also extends the `proof-assistant-settings' list.
 ;;;***
 
 ;;;### (autoloads (pg-pgip-askprefs pg-pgip-maybe-askpgip pg-pgip-process-packet)
-;;;;;;  "pg-pgip" "pg-pgip.el" (20118 50210))
+;;;;;;  "pg-pgip" "pg-pgip.el" (20123 64607))
 ;;; Generated autoloads from pg-pgip.el
 
 (autoload 'pg-pgip-process-packet "pg-pgip" "\
@@ -369,7 +369,7 @@ See `pg-next-error-regexp'.
 ;;;;;;  pg-slow-fontify-tracing-hint proof-electric-terminator-enable
 ;;;;;;  proof-define-assistant-command-witharg proof-define-assistant-command
 ;;;;;;  proof-process-buffer proof-goto-point proof-script-new-command-advance)
-;;;;;;  "pg-user" "pg-user.el" (20123 64108))
+;;;;;;  "pg-user" "pg-user.el" (20123 64158))
 ;;; Generated autoloads from pg-user.el
 
 (autoload 'proof-script-new-command-advance "pg-user" "\
@@ -619,7 +619,7 @@ in future if we have just activated it for this buffer.
 ;;;;;;  proof-register-possibly-new-processed-file pg-set-span-helphighlights
 ;;;;;;  proof-locked-region-empty-p proof-locked-region-full-p proof-unprocessed-begin
 ;;;;;;  proof-colour-locked) "proof-script" "proof-script.el" (20123
-;;;;;;  63408))
+;;;;;;  64988))
 ;;; Generated autoloads from proof-script.el
 
 (autoload 'proof-colour-locked "proof-script" "\
@@ -1025,7 +1025,7 @@ Return a unicode encoded version presentation of STR.
 ;;;;;;  "../lib/proof-compat.el" "../lib/span.el" "pg-autotest.el"
 ;;;;;;  "pg-custom.el" "pg-pbrpm.el" "pg-vars.el" "proof-auxmodes.el"
 ;;;;;;  "proof-config.el" "proof-faces.el" "proof-useropts.el" "proof.el"
-;;;;;;  "proofgeneral-pkg.el") (20123 64110 868313))
+;;;;;;  "proofgeneral-pkg.el") (20123 65399 608731))
 
 ;;;***