Fix incorrect uses of defvar

It didn't really matter that these variables were defined and set to nil during
compilation, since we ran compilation in a clean Emacs in --batch mode; it does
matter now, however, since package.el compiles PG in the user's currently
running Emacs instance.

15 files changed, 40 insertions, 59 deletions

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 72a16881..48772889 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -19,8 +19,8 @@
 (eval-when (compile)
   ;;(defvar coq-pre-v85 nil)
   (require 'compile)
-  (defvar coq-confirm-external-compilation nil); defpacustom
-  (defvar coq-compile-parallel-in-background nil) ; defpacustom
+  (defvar coq-confirm-external-compilation); defpacustom
+  (defvar coq-compile-parallel-in-background) ; defpacustom
   (proof-ready-for-assistant 'coq))     ; compile for coq
 
 
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index e5179390..878fb895 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -22,7 +22,7 @@
 ;     (message "%.06f" (float-time (time-since time)))))
 
 (eval-when-compile
-  (defvar coq-script-indent nil))
+  (defvar coq-script-indent))
 
 (defconst coq-any-command-regexp
   (proof-regexp-alt-list coq-keywords))
diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index 846371b4..cd29e218 100644
--- a/coq/coq-local-vars.el
+++ b/coq/coq-local-vars.el
@@ -15,8 +15,8 @@
   (require 'cl))
 
 (eval-when (compile)
-  (defvar coq-prog-name nil)
-  (defvar coq-load-path nil))
+  (defvar coq-prog-name)
+  (defvar coq-load-path))
 
 
 ;;; Code:
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index f9b317c2..fbe38a1e 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -28,10 +28,10 @@
   (require 'proof-compat))
 
 (eval-when (compile)
-  (defvar queueitems nil)       ; dynamic scope in p-s-extend-queue-hook
-  (defvar coq-compile-before-require nil)       ; defpacustom
-  (defvar coq-compile-parallel-in-background nil) ; defpacustom
-  (defvar coq-confirm-external-compilation nil)); defpacustom
+  (defvar queueitems)       ; dynamic scope in p-s-extend-queue-hook
+  (defvar coq-compile-before-require)       ; defpacustom
+  (defvar coq-compile-parallel-in-background) ; defpacustom
+  (defvar coq-confirm-external-compilation)); defpacustom
 
 (require 'coq-compile-common)
 
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index a1b2d30a..5ecfbf4b 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -19,10 +19,10 @@
   (require 'proof-compat))
 
 (eval-when (compile)
-  (defvar queueitems nil)       ; dynamic scope in p-s-extend-queue-hook
-  (defvar coq-compile-before-require nil)       ; defpacustom
-  (defvar coq-compile-parallel-in-background nil)       ; defpacustom
-  (defvar coq-confirm-external-compilation nil)); defpacustom
+  (defvar queueitems)       ; dynamic scope in p-s-extend-queue-hook
+  (defvar coq-compile-before-require)       ; defpacustom
+  (defvar coq-compile-parallel-in-background)       ; defpacustom
+  (defvar coq-confirm-external-compilation)); defpacustom
 
 (require 'coq-compile-common)
 
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 5844be74..fc0e547a 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -9,14 +9,9 @@
 (require 'proof-syntax)
 (require 'proof-utils)                  ; proof-locate-executable
 (require 'coq-db)
+(require 'span)
 
-(eval-when-compile
-  (require 'span)
-  (defvar coq-goal-command-regexp nil)
-  (defvar coq-save-command-regexp-strict nil))
-
-
- ;;; keyword databases
+;;; keyword databases
 
 (defcustom coq-user-tactics-db nil
   "User defined tactic information.  See `coq-syntax-db' for
diff --git a/coq/coq-system.el b/coq/coq-system.el
index aad7d386..67081ea4 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -20,8 +20,8 @@
   (proof-ready-for-assistant 'coq))
 
 (eval-when (compile)
-  (defvar coq-prog-args nil)
-  (defvar coq-debug nil))
+  (defvar coq-prog-args)
+  (defvar coq-debug))
 
 (defcustom coq-prog-env nil
   "List of environment settings d to pass to Coq process.
diff --git a/coq/coq.el b/coq/coq.el
index 0c366df5..16e69d00 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -19,18 +19,18 @@
   (require 'newcomment)
   (require 'etags)
   (unless (proof-try-require 'smie)
-    (defvar smie-indent-basic nil)
-    (defvar smie-rules-function nil))
-  (defvar proof-info nil)       ; dynamic scope in proof-tree-urgent-action
-  (defvar action nil)       ; dynamic scope in coq-insert-as stuff
-  (defvar string nil)       ; dynamic scope in coq-insert-as stuff
-  (defvar old-proof-marker nil)
-                         ; dynamic scoq in coq-proof-tree-enable-evar-callback
-  (defvar coq-auto-insert-as nil)    ; defpacustom
-  (defvar coq-time-commands nil)        ; defpacustom
+    (defvar smie-indent-basic)
+    (defvar smie-rules-function))
+  (defvar proof-info)       ; dynamic scope in proof-tree-urgent-action
+  (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-auto-insert-as)    ; defpacustom
+  (defvar coq-time-commands)        ; defpacustom
   (defvar coq-use-project-file t)        ; defpacustom
-  (defvar coq-use-editing-holes nil)    ; defpacustom
-  (defvar coq-hide-additional-subgoals nil) ; defpacustom
+  (defvar coq-use-editing-holes)    ; defpacustom
+  (defvar coq-hide-additional-subgoals)
   (proof-ready-for-assistant 'coq))     ; compile for coq
 
 (require 'proof)
@@ -1199,7 +1199,7 @@ flag Printing All set."
 
 ;; Check
 (eval-when (compile)
-  (defvar coq-auto-adapt-printing-width nil)); defpacustom
+  (defvar coq-auto-adapt-printing-width)); defpacustom
 
 ;; Since Printing Width is a synchronized option in coq (?) it is retored
 ;; silently to a previous value when retracting. So we reset the stored width
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index 4958b360..4bc61c15 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -260,7 +260,7 @@ This macro also extends the `proof-assistant-settings' list."
   (eval-when-compile
     (if (boundp 'proof-assistant-symbol)
 	;; declare variable to compiler to prevent warnings
-	(eval `(defvar ,(proof-ass-sym name) nil "Dummy for compilation."))))
+	(eval `(defvar ,(proof-ass-sym name)))))
   `(proof-defpacustom-fn (quote ,name) (quote ,val) (quote ,args)))
 
 
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index df617347..f029afcb 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -10,23 +10,13 @@
 (require 'cl)				; mapcan
 
 ;;; Code:
-(eval-when (compile)
-  (defvar proof-assistant-menu nil) ; defined by macro in proof-menu-define-specific
-  (defvar proof-mode-map nil))
-
-(require 'proof-utils)    ; proof-deftoggle, proof-eval-when-ready-for-assistant
-(require 'proof-useropts)
-(require 'proof-config)
-
-
-    
-
-
 (eval-when-compile
   (defvar proof-assistant-menu)	  ; defined by macro in proof-menu-define-specific
   (defvar proof-mode-map))
-    
 
+(require 'proof-utils)    ; proof-deftoggle, proof-eval-when-ready-for-assistant
+(require 'proof-useropts)
+(require 'proof-config)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 671c3c82..17ca325c 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -163,7 +163,7 @@ You can use customize to set this variable."
 (require 'proof-autoloads)
 
 (eval-when-compile
-  (defvar Info-dir-contents nil))
+  (defvar Info-dir-contents))
 
 ;; Add the info directory to the Info path
 (if (file-exists-p proof-info-directory) ; for safety
diff --git a/lib/holes.el b/lib/holes.el
index 09eb9dde..c0a864b0 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -30,9 +30,7 @@
 ;;
 ;; See documentation of `holes-mode'.
 
-
-(eval-when-compile 
-  (require 'span))
+(require 'span)
 (require 'cl)
 
 ;;; Code:
diff --git a/lib/proof-compat.el b/lib/proof-compat.el
index 1816ed0e..4eb942cb 100644
--- a/lib/proof-compat.el
+++ b/lib/proof-compat.el
@@ -17,9 +17,7 @@
 ;; Since Proof General 4.0, XEmacs is not supported at all.
 ;;
 
-(eval-when-compile
-  (require 'easymenu))
-
+(require 'easymenu)
 (require 'cl)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/phox/phox-tags.el b/phox/phox-tags.el
index 603622a6..73ed659b 100644
--- a/phox/phox-tags.el
+++ b/phox/phox-tags.el
@@ -18,9 +18,9 @@
 (require 'etags)
 
 (eval-when-compile
-  (defvar phox-doc-dir nil)
-  (defvar phox-lib-dir nil)
-  (defvar phox-etags nil))
+  (defvar phox-doc-dir)
+  (defvar phox-lib-dir)
+  (defvar phox-etags))
 
 
 (defun phox-tags-add-table(table)
diff --git a/phox/phox.el b/phox/phox.el
index 27b9cac0..79b8e747 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -7,7 +7,7 @@
 ;; loaded).
 
 (eval-when-compile
-  (defvar phox-toolbar-entries nil))
+  (defvar phox-toolbar-entries))
 
 (eval-after-load "pg-custom"
   '(setq phox-toolbar-entries