From 4835077e41fd8651e84eb2add7c7e85f50c8a646 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 26 Apr 2007 18:41:52 +0000
Subject: Fixed the "Time Qed." mistreating (now recognized as a save command
 and make spans agregation ok).

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

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index cf72ecac..0c871c3b 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -813,11 +813,15 @@ Used by `coq-goal-command-p'"
 ;; It is understood here as being a goal.  This is important for
 ;; recognizing global identifiers, see coq-global-p.
 (defconst coq-save-command-regexp-strict
-  (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-save-strict)))
+  (proof-anchor-regexp 
+   (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict)
+           "\\)")))
 (defconst coq-save-command-regexp
-  (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-save)))
+  (proof-anchor-regexp 
+   (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save)
+           "\\)")))
 (defconst coq-save-with-hole-regexp
-  (concat "\\(" (proof-ids-to-regexp coq-keywords-save-strict)
+  (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict)
 	  "\\)\\s-+\\(" coq-id "\\)\\s-*\\."))
 
 (defconst coq-goal-command-regexp
-- 
cgit v1.2.3