From 32a5ff235e9c61ffe784c557c27c4f586df72bd4 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 13 Sep 1999 14:01:18 +0000
Subject: Set proof-{qed,save}-commands.

---
 coq/coq.el | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 97f1e86c..043b7f15 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -424,9 +424,13 @@
 
   (setq proof-guess-command-line 'coq-guess-command-line)
 
+  ;; Commands sent to proof engine
   (setq proof-prf-string "Show"
 	proof-ctxt-string "Print All"
-	proof-help-string "Help")
+	proof-help-string "Help"
+	proof-goal-command "Goal %s."
+	proof-save-command "Save %s."
+	proof-kill-goal-command coq-kill-goal-command)
 
   (setq proof-goal-command-p 'coq-goal-command-p
 	proof-count-undos-fn 'coq-count-undos
@@ -440,7 +444,6 @@
   (setq proof-save-command-regexp coq-save-command-regexp
 	proof-save-with-hole-regexp coq-save-with-hole-regexp
 	proof-goal-with-hole-regexp coq-goal-with-hole-regexp
-	proof-kill-goal-command coq-kill-goal-command
 	proof-indent-commands-regexp (proof-ids-to-regexp coq-keywords))
 
   (coq-init-syntax-table)
-- 
cgit v1.2.3