diff options
| -rw-r--r-- | coq/coq.el | 8 | ||||
| -rw-r--r-- | lego/lego.el | 8 |
2 files changed, 10 insertions, 6 deletions
@@ -86,15 +86,17 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (define-derived-mode coq-shell-mode proof-shell-mode - "coq-shell" "Inferior shell mode for coq shell" + "coq-shell" + ;; With nil argument for docstring, Emacs makes up a nice one. + nil (coq-shell-mode-config)) (define-derived-mode coq-mode proof-mode - "coq" "Coq Mode" + "coq" nil (coq-mode-config)) (define-derived-mode coq-pbp-mode pbp-mode - "pbp" "Proof-by-pointing support for Coq" + "pbp" nil (coq-pbp-mode-config)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/lego/lego.el b/lego/lego.el index aed76bdf..82ec26ae 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -169,17 +169,19 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (define-derived-mode lego-shell-mode proof-shell-mode - "lego-shell" "Inferior shell mode for lego shell" + "lego-shell" + ;; With nil argument for docstring, Emacs makes up a nice one. + nil (lego-shell-mode-config)) (define-derived-mode lego-mode proof-mode - "lego" "Lego Mode" + "lego" nil (lego-mode-config) (easy-menu-change (list proof-mode-name) (car proof-help-menu) (append (cdr proof-help-menu) lego-help-menu-list))) (define-derived-mode lego-pbp-mode pbp-mode - "pbp" "Proof-by-pointing support for LEGO" + "pbp" nil (lego-pbp-mode-config)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |