From 813c9a3268b9b18a00d475281a35bc29b36688d3 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 6 Oct 1999 11:11:26 +0000
Subject: Fixed proof-showproof-command

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

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index 2aa751a9..a2df7a0c 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -414,7 +414,7 @@
   (setq proof-guess-command-line 'coq-guess-command-line)
 
   ;; Commands sent to proof engine
-  (setq proof-proof-command "Show"
+  (setq proof-showproof-command "Show"
 	proof-context-command "Print All"
 	proof-goal-command "Goal %s."
 	proof-save-command "Save %s."
@@ -424,6 +424,7 @@
 	proof-kill-goal-command coq-kill-goal-command)
 
   (setq proof-goal-command-p 'coq-goal-command-p
+	proof-nested-goals-allowed t
 	proof-count-undos-fn 'coq-count-undos
 	proof-find-and-forget-fn 'coq-find-and-forget
         proof-goal-hyp-fn 'coq-goal-hyp
-- 
cgit v1.2.3