From c1f6c9c2f87edea03d9c279719f0f4a10c396db0 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Sat, 25 Feb 2017 19:55:51 -0500
Subject: 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!")
---
 coq/coq-compile-common.el | 18 ++++++++++++------
 coq/coq-par-compile.el    |  5 +----
 coq/coq-seq-compile.el    |  5 +----
 3 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index c557f474..f6adc5cd 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -32,7 +32,7 @@
 ;; coq-par-compile, respectively. However, the :initialization
 ;; function of a defcustom seems to be evaluated when reading the
 ;; defcustom form. Therefore, these functions must be defined already,
-;; when the defpacustum coq-compile-parallel-in-background is read.
+;; when the defcustom coq-compile-parallel-in-background is read.
 
 (defun coq-par-enable ()
   "Enable parallel compilation.
@@ -155,7 +155,7 @@ Ignore any quick setting for Coq versions before 8.5."
   :group 'coq
   :package-version '(ProofGeneral . "4.1"))
 
-(defpacustom compile-before-require nil
+(defcustom coq-compile-before-require nil
   "If non-nil, check dependencies of required modules and compile if necessary.
 If non-nil ProofGeneral intercepts \"Require\" commands and checks if the
 required library module and its dependencies are up-to-date. If not, they
@@ -167,7 +167,9 @@ This option can be set/reset via menu
   :safe 'booleanp
   :group 'coq-auto-compile)
 
-(defpacustom compile-parallel-in-background nil
+(proof-deftoggle coq-compile-before-require)
+
+(defcustom coq-compile-parallel-in-background nil
   "Choose the internal compilation method.
 When Proof General compiles itself, you have the choice between
 two implementations. If this setting is nil, then Proof General
@@ -182,8 +184,12 @@ This option can be set/reset via menu
 `Coq -> Auto Compilation -> Compile Parallel In Background'."
   :type 'boolean
   :safe 'booleanp
-  :group 'coq-auto-compile
-  :eval (coq-switch-compilation-method))
+  :group 'coq-auto-compile)
+
+(proof-deftoggle coq-compile-parallel-in-background)
+
+(defun coq-compile-parallel-in-background ()
+  (coq-switch-compilation-method))
 
 ;; defpacustom fails to call :eval during inititialization, see trac #456
 (coq-switch-compilation-method)
@@ -405,7 +411,7 @@ This option can be set via menu
 ;; define coq-lock-ancestors-toggle
 (proof-deftoggle coq-lock-ancestors)
 
-(defpacustom confirm-external-compilation t
+(defcustom coq-confirm-external-compilation t
   "If set let user change and confirm the compilation command.
 Otherwise start the external compilation without confirmation.
 
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index fbe38a1e..05703e45 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -28,10 +28,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)
 
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)
 
-- 
cgit v1.2.3