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 ++-
 isar/isar.el | 2 +-
 lego/lego.el | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

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
diff --git a/isar/isar.el b/isar/isar.el
index 1c529bc3..9b00c6ca 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -158,7 +158,7 @@
    proof-save-with-hole-regexp  isar-save-with-hole-regexp
    proof-indent-commands-regexp	isar-indent-regexp
    ;; proof engine commands
-   proof-proof-command		"pr"
+   proof-showproof-command	"pr"
    proof-goal-command		"lemma \"%s\";"
    proof-save-command		"qed"
    proof-context-command		"print_context"
diff --git a/lego/lego.el b/lego/lego.el
index 5930f501..bf906c9f 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -349,7 +349,7 @@ Checks the width in the `proof-goals-buffer'"
 
   (setq proof-mode-for-script 'lego-mode)
 
-  (setq proof-proof-command "Prf"
+  (setq proof-showproof-command "Prf"
 	proof-goal-command "Goal %s;"
 	proof-save-command "Save %s;"
 	proof-context-command "Ctxt"
-- 
cgit v1.2.3