Change (eval-when (compile) ...) to (eval-when-compile ...)

This fixes a bunch of compilation warnings

coq/coq-compile-common.el

@@ -17,7 +17,7 @@
 (require 'coq-system)
 (require 'compile)
 
-(eval-when (compile)
+(eval-when-compile
   ;;(defvar coq-pre-v85 nil)
   (defvar coq-confirm-external-compilation); defpacustom
   (defvar coq-compile-parallel-in-background)) ; defpacustom

coq/coq-local-vars.el

@@ -14,7 +14,7 @@
 (eval-when-compile
   (require 'cl))
 
-(eval-when (compile)
+(eval-when-compile
   (defvar coq-prog-name)
   (defvar coq-load-path))
 

coq/coq-par-compile.el

@@ -27,7 +27,7 @@
 (eval-when-compile
   (require 'proof-compat))
 
-(eval-when (compile)
+(eval-when-compile
   (defvar queueitems))       ; dynamic scope in p-s-extend-queue-hook
 
 (require 'coq-compile-common)

coq/coq-seq-compile.el

@@ -18,7 +18,7 @@
 (eval-when-compile
   (require 'proof-compat))
 
-(eval-when (compile)
+(eval-when-compile
   (defvar queueitems))       ; dynamic scope in p-s-extend-queue-hook
 
 (require 'coq-compile-common)

coq/coq-system.el

@@ -18,7 +18,7 @@
   (require 'cl)
   (require 'proof-compat))
 
-(eval-when (compile)
+(eval-when-compile
   (defvar coq-prog-args)
   (defvar coq-debug))
 

coq/coq.el

@@ -12,7 +12,7 @@
   (require 'cl)
   (require 'proof-compat))
 
-(eval-when (compile)
+(eval-when-compile
   (require 'proof-utils)
   (require 'span)
   (require 'outline)
@@ -25,10 +25,11 @@
   (defvar action)       ; dynamic scope in coq-insert-as stuff
   (defvar string)       ; dynamic scope in coq-insert-as stuff
   (defvar old-proof-marker)
-                                        ; dynamic scoq in coq-proof-tree-enable-evar-callback
+  (defvar coq-keymap)
+  (defvar coq-one-command-per-line)
   (defvar coq-auto-insert-as)    ; defpacustom
   (defvar coq-time-commands)        ; defpacustom
-  (defvar coq-use-project-file t)        ; defpacustom
+  (defvar coq-use-project-file)        ; defpacustom
   (defvar coq-use-editing-holes)    ; defpacustom
   (defvar coq-hide-additional-subgoals))
 
@@ -1193,7 +1194,7 @@ flag Printing All set."
   (coq-ask-do-show-all "Show goal number" "Show" t))
 
 ;; Check
-(eval-when (compile)
+(eval-when-compile
   (defvar coq-auto-adapt-printing-width)); defpacustom
 
 ;; Since Printing Width is a synchronized option in coq (?) it is retored

generic/proof-autoloads.el

@@ -7,7 +7,7 @@
 (eval-when-compile
   (require 'cl))
 
-(eval-when (compile)
+(eval-when-compile
   (require 'pg-vars)
   (require 'proof-config)
   (require 'scomint))

generic/proof-maths-menu.el

@@ -23,7 +23,7 @@
 (eval-when-compile
   (require 'cl))
 
-(eval-when (compile)
+(eval-when-compile
   (require 'proof-auxmodes)	  ; loaded by proof.el
   (require 'maths-menu))	  ; loaded dynamically in proof-auxmodes
 

generic/proof-mmm.el

@@ -28,7 +28,7 @@
 (eval-when-compile
   (require 'cl))
 
-(eval-when (compile)
+(eval-when-compile
   (require 'proof-auxmodes)	  ; will be loaded
   (require 'mmm-auto))		  ; loaded dynamically by proof-auxmodes
 

generic/proof-shell.el

@@ -27,7 +27,7 @@
 (declare-function proof-tree-urgent-action "proof-tree" (flags))
 (declare-function proof-tree-handle-delayed-output "proof-tree"
 		  (old-proof-marker cmd flags span))
-(eval-when (compile)
+(eval-when-compile
   ;; without the nil initialization the compiler still warns about this variable
   (defvar proof-tree-external-display nil))
 

generic/proof-tree.el

@@ -88,7 +88,7 @@
 
 (require 'cl)
 
-(eval-when (compile)
+(eval-when-compile
   (require 'proof-shell))
 
 

generic/proof-unicode-tokens.el

@@ -21,10 +21,10 @@
 (eval-when-compile
   (require 'cl))
 
-(eval-when (compile)
-    (require 'scomint)
-    (require 'proof-auxmodes)	 ; loaded by proof.el, autoloads us
-    (require 'unicode-tokens))	 ; it will be loaded by proof-auxmodes
+(eval-when-compile
+  (require 'scomint)
+  (require 'proof-auxmodes)	 ; loaded by proof.el, autoloads us
+  (require 'unicode-tokens))	 ; it will be loaded by proof-auxmodes
 
 (require 'proof-config)			; config variables
 

hol-light/hol-light.el

@@ -16,9 +16,9 @@
 (or (proof-try-require 'caml-font)	  ; use OCaml Emacs mode syntax 
     (defvar caml-font-lock-keywords nil)) ;
 
-(eval-when (compile)
- (require 'proof-tree)
- (defvar caml-font-lock-keywords nil))
+(eval-when-compile
+  (require 'proof-tree)
+  (defvar caml-font-lock-keywords nil))
 
 (defcustom hol-light-home 
   (or (getenv "HOLLIGHT_HOME")

isar/isabelle-system.el

@@ -15,7 +15,7 @@
 (eval-when-compile
   (require 'cl))			;  mapcan, eval-when
 
-(eval-when (compile)
+(eval-when-compile
   (require 'span)
   (require 'scomint)
   (require 'proof-site)

isar/isar-autotest.el

@@ -10,7 +10,7 @@
 
 (require 'pg-autotest)
 
-(eval-when (compile)
+(eval-when-compile
   (require 'cl))
 
 (require 'proof-site)

isar/isar-unicode-tokens.el

@@ -14,7 +14,7 @@
 
 (require 'cl)				; for-loop
 
-(eval-when (compile)
+(eval-when-compile
   (require 'unicode-tokens)	    ; it's loaded dynamically at runtime
   (require 'proof-unicode-tokens))  ; that file loads us at runtime
 

isar/isar.el

@@ -19,7 +19,7 @@
 (eval-when-compile 
   (require 'cl))
 
-(eval-when (compile)
+(eval-when-compile
   (require 'span)
   (require 'proof-syntax)
   (require 'pg-goals)

lib/pg-dev.el

@@ -19,7 +19,7 @@
 (eval-when-compile
   (require 'cl))
 
-(eval-when (compile)
+(eval-when-compile
   (require 'proof-site))
 
 (with-no-warnings

phox/phox-extraction.el

@@ -9,7 +9,7 @@
 
 (require 'cl)
 
-(eval-when (compile)
+(eval-when-compile
   (defvar phox-prog-name nil))
 
 (declare-function proof-shell-invisible-command "proof-shell" (str))