aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-seq-compile.el
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2017-02-25 19:55:51 -0500
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2017-03-08 15:06:17 -0500
commitc1f6c9c2f87edea03d9c279719f0f4a10c396db0 (patch)
treecb55f1e0fa7c086a53e75929b4fdcfaa2d7b89b0 /coq/coq-seq-compile.el
parent031a5780575f3b87124df303b42e202aa5e1c418 (diff)
Remove uses of defpacustom in coq-compile-common
This file is `require'-d from other places, at compile time. This doesn't work nicely with compilation by package.el (PG complains and says "defpacustom: Proof assistant setting compile-before-require re-defined!")
Diffstat (limited to 'coq/coq-seq-compile.el')
-rw-r--r--coq/coq-seq-compile.el5
1 files changed, 1 insertions, 4 deletions
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index 5ecfbf4b..ee4181ae 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -19,10 +19,7 @@
(require 'proof-compat))
(eval-when (compile)
- (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
+ (defvar queueitems)) ; dynamic scope in p-s-extend-queue-hook
(require 'coq-compile-common)