diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2007-04-26 18:41:52 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2007-04-26 18:41:52 +0000 |
| commit | 4835077e41fd8651e84eb2add7c7e85f50c8a646 (patch) | |
| tree | 1084fbd38f39a3722b441266b8894e4fc0c0c60d | |
| parent | 9c6280e42ae79fd8b5be853971f87ff362b00c4a (diff) | |
Fixed the "Time Qed." mistreating (now recognized as a save command
and make spans agregation ok).
| -rw-r--r-- | coq/coq-syntax.el | 10 |
1 files 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 |