From d3170a0cbe470cd620bc16e04eb148e554047d35 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
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'.
---
 generic/pg-pamacs.el | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'generic')

diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index 8b9b83c7..d7bb1bf3 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -155,6 +155,8 @@ Usage: (defpgdefault SYM VALUE)"
 ;;;###autoload
 (defun proof-defpacustom-fn (name val args)
   "As for macro `defpacustom' but evaluating arguments."
+  (unless (and proof-assistant (not (string= proof-assistant "")))
+    (error "No proof assistant defined"))
   (let (newargs setting evalform type descr)
     (while args
       (cond
-- 
cgit v1.2.3