From 659646acf6c78bf1975cd1032b822d4a6179637e Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 1 Oct 1999 10:22:56 +0000
Subject: Disable proof-help-string, was set to an invalid command.

---
 coq/coq.el | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/coq/coq.el b/coq/coq.el
index ca0f11cb..4e6767f2 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -427,10 +427,11 @@
   ;; Commands sent to proof engine
   (setq proof-prf-string "Show"
 	proof-ctxt-string "Print All"
-	proof-help-string "Help"
 	proof-goal-command "Goal %s."
 	proof-save-command "Save %s."
 	proof-find-theorems-command "Search %s."
+;; FIXME da: Does Coq have a help or about command?
+;;	proof-help-string "Help"
 	proof-kill-goal-command coq-kill-goal-command)
 
   (setq proof-goal-command-p 'coq-goal-command-p
-- 
cgit v1.2.3