Loading `pg-custom` breaks PG

[monnier]

If for some reason Emacs loads pg-custom.el before we load coq.el, PG becomes unusable. In my case loading coq.el gives me an error about coq-toolbar-entries being a void variable.

This is because pg-custom.el uses proof-assistant-symbol to decide the name of the variables it defines, so if it's loaded before proof-assistant-symbol is set, it defines variables with the wrong name (presumably things like nil-toolbar-entries.

This is related to the lack of support for the use of PG with several different provers in a single Emacs session. The patch below seems to fix my immediate problem without tackling that larger issue.

diff --git a/generic/proof-script.el b/generic/proof-script.el
index b7d456e84b..9ddb90b036 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -109,7 +109,10 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
        (setq proof-assistant ,assistant-name)
        (setq proof-assistant-symbol (quote ,assistantsym))
        ;; define the per-prover settings which depend on above
-       (require 'pg-custom)
+       ;; If that file was loaded already (i.e. before setting
+       ;; `proof-assistant-symbol'), it did not define the right variables, so
+       ;; use `load' rather than `require'.
+       (load "pg-custom" nil 'nomessage)
        (setq proof-mode-for-shell (proof-ass-sym shell-mode))
        (setq proof-mode-for-response (proof-ass-sym response-mode))
        (setq proof-mode-for-goals (proof-ass-sym goals-mode))