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 /coq/coq-abbrev.el | |
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 'coq/coq-abbrev.el')
-rw-r--r-- | coq/coq-abbrev.el | 10 |
1 files changed, 4 insertions, 6 deletions
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) |