From 2bf4a7f0b3cf660c6b215a3e49d80115409e192e Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 28 Aug 2001 15:53:17 +0000
Subject: Change of proof span type back to goalsave

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

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index 6e2325f1..be65c1cd 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -203,7 +203,7 @@
 
        ((eq (span-property span 'type) 'comment))       
 
-       ((eq (span-property span 'type) 'proof)
+       ((eq (span-property span 'type) 'goalsave)
 	;; Note da 6.10.99: in Lego and Isabelle, it's trivial to
 	;; forget an unnamed theorem.  Coq really does use the 
 	;; identifier "Unnamed_thm", though!  So we don't need
-- 
cgit v1.2.3