diff options
| -rw-r--r-- | coq/coq-compile-common.el | 2 | ||||
| -rw-r--r-- | coq/coq-local-vars.el | 2 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 2 | ||||
| -rw-r--r-- | coq/coq-seq-compile.el | 2 | ||||
| -rw-r--r-- | coq/coq-system.el | 2 | ||||
| -rw-r--r-- | coq/coq.el | 9 | ||||
| -rw-r--r-- | generic/proof-autoloads.el | 2 | ||||
| -rw-r--r-- | generic/proof-maths-menu.el | 2 | ||||
| -rw-r--r-- | generic/proof-mmm.el | 2 | ||||
| -rw-r--r-- | generic/proof-shell.el | 2 | ||||
| -rw-r--r-- | generic/proof-tree.el | 2 | ||||
| -rw-r--r-- | generic/proof-unicode-tokens.el | 8 | ||||
| -rw-r--r-- | hol-light/hol-light.el | 6 | ||||
| -rw-r--r-- | isar/isabelle-system.el | 2 | ||||
| -rw-r--r-- | isar/isar-autotest.el | 2 | ||||
| -rw-r--r-- | isar/isar-unicode-tokens.el | 2 | ||||
| -rw-r--r-- | isar/isar.el | 2 | ||||
| -rw-r--r-- | lib/pg-dev.el | 2 | ||||
| -rw-r--r-- | phox/phox-extraction.el | 2 |
19 files changed, 28 insertions, 27 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index f6adc5cd..f96b07da 100644 --- a/coq/coq-compile-common.el +++ b/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 diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el index cd29e218..50a1f626 100644 --- a/coq/coq-local-vars.el +++ b/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)) diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 05703e45..1580febd 100644 --- a/coq/coq-par-compile.el +++ b/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) diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index ee4181ae..bf492f82 100644 --- a/coq/coq-seq-compile.el +++ b/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) diff --git a/coq/coq-system.el b/coq/coq-system.el index ad85a960..9d6a9589 100644 --- a/coq/coq-system.el +++ b/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)) @@ -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 diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el index 90430f73..ba8d1f05 100644 --- a/generic/proof-autoloads.el +++ b/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)) diff --git a/generic/proof-maths-menu.el b/generic/proof-maths-menu.el index ded6568a..57fafa98 100644 --- a/generic/proof-maths-menu.el +++ b/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 diff --git a/generic/proof-mmm.el b/generic/proof-mmm.el index b450f20c..5d904ce3 100644 --- a/generic/proof-mmm.el +++ b/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 diff --git a/generic/proof-shell.el b/generic/proof-shell.el index f79b78c2..7d3fe5b9 100644 --- a/generic/proof-shell.el +++ b/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)) diff --git a/generic/proof-tree.el b/generic/proof-tree.el index f0894656..438c035e 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -88,7 +88,7 @@ (require 'cl) -(eval-when (compile) +(eval-when-compile (require 'proof-shell)) diff --git a/generic/proof-unicode-tokens.el b/generic/proof-unicode-tokens.el index 3f9f0199..0352f012 100644 --- a/generic/proof-unicode-tokens.el +++ b/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 diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index 85d10607..467453ed 100644 --- a/hol-light/hol-light.el +++ b/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") diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el index d4ef3762..e399474b 100644 --- a/isar/isabelle-system.el +++ b/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) diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index 091d2a0a..f8784bc2 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -10,7 +10,7 @@ (require 'pg-autotest) -(eval-when (compile) +(eval-when-compile (require 'cl)) (require 'proof-site) diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el index a1e05843..c6f58452 100644 --- a/isar/isar-unicode-tokens.el +++ b/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 diff --git a/isar/isar.el b/isar/isar.el index b8119ee6..bb755d4f 100644 --- a/isar/isar.el +++ b/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) diff --git a/lib/pg-dev.el b/lib/pg-dev.el index 3bbda049..e11d15ff 100644 --- a/lib/pg-dev.el +++ b/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 diff --git a/phox/phox-extraction.el b/phox/phox-extraction.el index 87ea70f6..84937f36 100644 --- a/phox/phox-extraction.el +++ b/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)) |