diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2017-02-25 20:15:09 -0500 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2017-03-08 15:06:17 -0500 |
| commit | d3170a0cbe470cd620bc16e04eb148e554047d35 (patch) | |
| tree | 308611adaa93c54ac0da111fa7956c080c7ab425 /generic | |
| parent | c1f6c9c2f87edea03d9c279719f0f4a10c396db0 (diff) | |
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'.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-pamacs.el | 2 |
1 files changed, 2 insertions, 0 deletions
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 |