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.

8 files changed, 29 insertions, 34 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