aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-abbrev.el
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coq-abbrev.el')
-rw-r--r--coq/coq-abbrev.el12
1 files changed, 5 insertions, 7 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 062f7580..79231ad9 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))
;;;;;
@@ -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
@@ -304,7 +304,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
`(
""
@@ -342,12 +342,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)