diff options
| -rw-r--r-- | coq/coq-compile-common.el | 4 | ||||
| -rw-r--r-- | coq/coq-indent.el | 2 | ||||
| -rw-r--r-- | coq/coq-local-vars.el | 4 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 8 | ||||
| -rw-r--r-- | coq/coq-seq-compile.el | 8 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 9 | ||||
| -rw-r--r-- | coq/coq-system.el | 4 | ||||
| -rw-r--r-- | coq/coq.el | 24 | ||||
| -rw-r--r-- | generic/pg-pamacs.el | 2 | ||||
| -rw-r--r-- | generic/proof-menu.el | 16 | ||||
| -rw-r--r-- | generic/proof-site.el | 2 | ||||
| -rw-r--r-- | lib/holes.el | 4 | ||||
| -rw-r--r-- | lib/proof-compat.el | 4 | ||||
| -rw-r--r-- | phox/phox-tags.el | 6 | ||||
| -rw-r--r-- | phox/phox.el | 2 |
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. @@ -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 |