Set nested goals; include Lemma again in def of goal.

1 files changed, 6 insertions, 1 deletions

diff --git a/coq/coq.el b/coq/coq.el
index bf6cbaa1..571b8bf6 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -198,7 +198,11 @@
   "Decide whether argument is a goal or not"
   (and (proof-string-match coq-goal-command-regexp str)
        (not (proof-string-match "Definition.*:=" str))
-       (not (proof-string-match "Lemma.*:=" str))))
+       ;; 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))))
+       ))
 
 ;; TODO : add the stuff to handle the "Correctness" command 
 
@@ -518,6 +522,7 @@ This is specific to coq-mode."
 	proof-kill-goal-command coq-kill-goal-command)
 
   (setq proof-goal-command-p 'coq-goal-command-p
+	proof-nested-goals-p t ;; da: new for 3.4
 	proof-count-undos-fn 'coq-count-undos
 	proof-find-and-forget-fn 'coq-find-and-forget
         proof-goal-hyp-fn 'coq-goal-hyp