Change of proof span type back to goalsave

1 files changed, 1 insertions, 1 deletions

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