From d4316a2d63c9c2b12cdce73e62cd435d7ff01002 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 6 Oct 1999 11:18:56 +0000
Subject: More improvements/fixes for closing unfinished proofs. Added
 proof-unnamed-theorem-name.

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

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index 4b0f6070..daa71eb6 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -190,8 +190,12 @@
        ((eq (span-property span 'type) 'comment))       
 
        ((eq (span-property span 'type) 'goalsave)
-	(setq ans (concat coq-forget-id-command
-			  (span-property span 'name) proof-terminal-string)))
+	;; FIXME da 5.10.99: I added in this test for an unnamed
+	;; theorem.  Probably it is harmless (it's a new case for LEGO
+	;; and Isabelle).
+	(unless (eq (span-property span 'name) proof-unnamed-theorem-name)
+	  (setq ans (concat lego-forget-id-command
+			    (span-property span 'name) proof-terminal-string))))
 
        ((proof-string-match (concat "\\`\\(" coq-keywords-decl-defn-regexp
                               "\\)\\s-*\\(" proof-id "\\)\\s-*[\\[,:]") str)
-- 
cgit v1.2.3