From 70dfbc54d9a6b559dbfcfd6105a7e8c80d78d888 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Sun, 26 Feb 2017 00:28:18 -0500
Subject: Fix incorrect assumption that noninteractive == byte-compiling

The PG Makefile does ensure (using --batch) that noninteractive is non-nil while
compiling, but package.el doesn't.
---
 coq/coq-abbrev.el   | 2 +-
 coq/coq-autotest.el | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'coq')

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 2b318dea..a05c9853 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -71,7 +71,7 @@
     ;; DA: how about above, just temporarily disable saving?
     (message "Coq default abbrevs loaded")))
 
-(unless noninteractive
+(unless (or noninteractive (bound-and-true-p byte-compile-current-file))
   (coq-install-abbrevs))
 ;;;;;
 
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index b6b361ed..a8367b5c 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -16,7 +16,7 @@
   (defvar coq-compile-before-require nil))
 
 
-(unless noninteractive
+(unless (bound-and-true-p byte-compile-current-file)
 
   (pg-autotest start 'debug)
 
-- 
cgit v1.2.3


From 33614d35a25b54c23171c360a61b913f0c1158ce Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Sat, 25 Feb 2017 19:06:26 -0500
Subject: 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.
---
 coq/coq-compile-common.el |  4 ++--
 coq/coq-indent.el         |  2 +-
 coq/coq-local-vars.el     |  4 ++--
 coq/coq-par-compile.el    |  8 ++++----
 coq/coq-seq-compile.el    |  8 ++++----
 coq/coq-syntax.el         |  9 ++-------
 coq/coq-system.el         |  4 ++--
 coq/coq.el                | 24 ++++++++++++------------
 8 files changed, 29 insertions(+), 34 deletions(-)

(limited to 'coq')

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
-- 
cgit v1.2.3


From 673082b2bee3ca327db56bdc559f7f925259d1c8 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Sat, 25 Feb 2017 19:18:16 -0500
Subject: Remove unnecessary calls to 'eval-and-compile'

---
 coq/coq.el | 26 +++++++++++---------------
 1 file changed, 11 insertions(+), 15 deletions(-)

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index 16e69d00..b60606c3 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -306,27 +306,23 @@ See also `coq-hide-additional-subgoals'."
 ;; Derived modes
 ;;
 
-(eval-and-compile ;; FIXME: Why?
-  (define-derived-mode coq-shell-mode proof-shell-mode
-    "Coq Shell" nil
-    (coq-shell-mode-config)))
+(define-derived-mode coq-shell-mode proof-shell-mode
+  "Coq Shell" nil
+  (coq-shell-mode-config))
 
-(eval-and-compile ;; FIXME: Why?
-  (define-derived-mode coq-response-mode proof-response-mode
+(define-derived-mode coq-response-mode proof-response-mode
   "Coq Response" nil
-    (coq-response-config)))
+  (coq-response-config))
 
-(eval-and-compile ;; FIXME: Why?
-  (define-derived-mode coq-mode proof-mode "Coq"
-    "Major mode for Coq scripts.
+(define-derived-mode coq-mode proof-mode "Coq"
+  "Major mode for Coq scripts.
 
 \\{coq-mode-map}"
-    (coq-mode-config)))
+  (coq-mode-config))
 
-(eval-and-compile ;; FIXME: Why?
-  (define-derived-mode coq-goals-mode proof-goals-mode
-    "Coq Goals" nil
-    (coq-goals-mode-config)))
+(define-derived-mode coq-goals-mode proof-goals-mode
+  "Coq Goals" nil
+  (coq-goals-mode-config))
 
 ;; Indentation and navigation support via SMIE.
 
-- 
cgit v1.2.3


From 98f2e463287e3562dc7b7126e062919a8604ca4a Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Sat, 25 Feb 2017 19:35:35 -0500
Subject: Remove compile-time calls to proof-ready-for-assistant

Compilation used to run in a separate Emacs process for each file, but that's not
what happens when installing PG with package.el.
---
 coq/coq-autotest.el       | 7 ++-----
 coq/coq-compile-common.el | 6 ++----
 coq/coq-system.el         | 3 +--
 coq/coq.el                | 3 +--
 4 files changed, 6 insertions(+), 13 deletions(-)

(limited to 'coq')

diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index a8367b5c..e3c4b978 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -10,11 +10,8 @@
 
 (require 'pg-autotest)
 
-(eval-when (compile)
-  (require 'proof-site)
-  (proof-ready-for-assistant 'coq)
-  (defvar coq-compile-before-require nil))
-
+(require 'proof-site)
+(defvar coq-compile-before-require)
 
 (unless (bound-and-true-p byte-compile-current-file)
 
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 48772889..c557f474 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -15,14 +15,12 @@
 
 (require 'proof-shell)
 (require 'coq-system)
+(require 'compile)
 
 (eval-when (compile)
   ;;(defvar coq-pre-v85 nil)
-  (require 'compile)
   (defvar coq-confirm-external-compilation); defpacustom
-  (defvar coq-compile-parallel-in-background) ; defpacustom
-  (proof-ready-for-assistant 'coq))     ; compile for coq
-
+  (defvar coq-compile-parallel-in-background)) ; defpacustom
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 67081ea4..ad85a960 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -16,8 +16,7 @@
 
 (eval-when-compile
   (require 'cl)
-  (require 'proof-compat)
-  (proof-ready-for-assistant 'coq))
+  (require 'proof-compat))
 
 (eval-when (compile)
   (defvar coq-prog-args)
diff --git a/coq/coq.el b/coq/coq.el
index b60606c3..2c8e4cfa 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -30,8 +30,7 @@
   (defvar coq-time-commands)        ; defpacustom
   (defvar coq-use-project-file t)        ; defpacustom
   (defvar coq-use-editing-holes)    ; defpacustom
-  (defvar coq-hide-additional-subgoals)
-  (proof-ready-for-assistant 'coq))     ; compile for coq
+  (defvar coq-hide-additional-subgoals))
 
 (require 'proof)
 (require 'coq-system)                   ; load path, option, project file etc.
-- 
cgit v1.2.3


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(-)

(limited to 'coq')

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


From d3170a0cbe470cd620bc16e04eb148e554047d35 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Sat, 25 Feb 2017 20:15:09 -0500
Subject: Remove uses of defpgdefault in coq-abbrev

This file is `require'-d when compiling coq.el, and at that point the proof
assistant isn't set to coq yet, so it would define variables prefixed by `nil-'
instead of `coq'.
---
 coq/coq-abbrev.el | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'coq')

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index a05c9853..30ec60c4 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -98,7 +98,7 @@ It was constructed with `proof-defstringset-fn'.")
 
 ;; The coq menu partly built from tables
 
-;; Common part (scrit, response and goals buffers)
+;; Common part (script, response and goals buffers)
 (defconst coq-menu-common-entries
   `(
     ["Toggle 3 Windows Mode" proof-three-window-toggle
@@ -300,7 +300,7 @@ It was constructed with `proof-defstringset-fn'.")
     ["ML4PG" (coq-activate-ml4pg) :help "Activates ML4PG: machine-learning methods for Proof General"]
     ))
 
-(defpgdefault menu-entries
+(setq-default coq-menu-entries
   (append coq-menu-common-entries
   `(
     ""
@@ -338,12 +338,10 @@ It was constructed with `proof-defstringset-fn'.")
      ["help" coq-local-vars-list-show-doc t]
      ["Compile" coq-Compile t]))))
 
-(defpgdefault help-menu-entries
+(setq-default coq-help-menu-entries
   '(["help on setting prog name persistently for a file" 
      coq-local-vars-list-show-doc t]))
 
-(defpgdefault other-buffers-menu-entries coq-menu-common-entries)
-
-
+(setq-default coq-other-buffers-menu-entries coq-menu-common-entries)
 
 (provide 'coq-abbrev)
-- 
cgit v1.2.3


From cb3f86402688e2f920d0cdc326874505d5e3aa6f Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Sat, 25 Feb 2017 20:16:28 -0500
Subject: Add a FIXME in coq.el

---
 coq/coq.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index 2c8e4cfa..deb40ec4 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1205,7 +1205,7 @@ flag Printing All set."
 ;; we can remove this.
 (defun coq-set-auto-adapt-printing-width (&optional symb val); args are for :set compatibility
   "Function called when setting `auto-adapt-printing-width'"
-  (setq symb val)
+  (setq symb val) ;; FIXME this is wrong (it should be 'set', but it would set nil sometimes)
   (if coq-auto-adapt-printing-width
       (progn
         (add-hook 'proof-assert-command-hook 'coq-adapt-printing-width)
-- 
cgit v1.2.3