From 7770e98ef03aba740fdf7d459aac51ce7f0f5993 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 12 Jun 2002 09:51:47 +0000
Subject: Add proof-nested-undo-regexp setting

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

diff --git a/coq/coq.el b/coq/coq.el
index 52222ac3..24b22824 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -209,8 +209,8 @@
        ;; da: 3.4 test: do not exclude Lemma: we want goal-command-p to
        ;; succeed for nested goals too now.
        ;; (should we also exclude Definition?)
-       ;; (not (proof-string-match "Lemma.*:=" str))))
-       ))
+       (not (proof-string-match "Lemma.*:=" str))))
+;; ))
 
 ;; TODO : add the stuff to handle the "Correctness" command 
 
@@ -547,7 +547,8 @@ This is specific to coq-mode."
 
   (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-goal-with-hole-regexp coq-goal-with-hole-regexp
+	proof-nested-undo-regexp coq-backable-commands-regexp)
   
   (setq	
    proof-indent-close-offset -1
-- 
cgit v1.2.3