From b3ee5d1189e7d4e680faaf707dd9245b40f9eb55 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 22 Sep 1998 13:27:47 +0000
Subject: Fixed docstrings for derived modes

---
 coq/coq.el   | 8 +++++---
 lego/lego.el | 8 +++++---
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index c8d13a74..45931ac3 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-- 
cgit v1.2.3