Fixed colorization bug #356, introduced by a previous fix of bug 140.

2 files changed, 7 insertions, 2 deletions

diff --git a/coq/coq-db.el b/coq/coq-db.el
index a91fb3c9..53ea970f 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -119,7 +119,7 @@ regexp.  See `coq-syntax-db' for DB structure."
 	(setq l tl)))
 ; da: next call is wrong?
 ;    (proof-ids-to-regexp res)))
-    (proof-regexp-alt-list res)))
+    (concat "\\_<\\(?:" (proof-regexp-alt-list res) "\\)\\_>")))
 
 
 ;; Computes the max length of strings in a list
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 1b469a93..f94cd4a2 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -836,6 +836,7 @@ Used by `coq-goal-command-p'"
   (append coq-state-changing-tactics coq-state-preserving-tactics))
 
 (defvar coq-tactics-regexp (coq-build-opt-regexp-from-db coq-tactics-db))
+;(defvar coq-tactics-regexp-symb (coq-build-opt-regexp-from-db coq-tactics-db))
 
 (defvar coq-retractable-instruct
   (append coq-state-changing-tactics coq-keywords-state-changing-commands))
@@ -849,6 +850,10 @@ Used by `coq-goal-command-p'"
 	  coq-keywords-defn coq-keywords-commands)
   "All keywords in a Coq script.")
 
+;; coq-build-opt-regexp-from-db already adds "\\_<" "\\_>"
+(defun proof-regexp-alt-list-symb (args)
+  (concat "\\_<" (proof-regexp-alt-list args) "\\_>"))
+
 (defvar coq-keywords-regexp (proof-regexp-alt-list coq-keywords))
 
 
@@ -975,7 +980,7 @@ Group number 1 matches the name of the library which is required.")
     (cons coq-reserved-regexp 'font-lock-type-face)
     (cons coq-tactics-regexp 'proof-tactics-name-face)
     (cons (proof-regexp-alt-list coq-tacticals) 'proof-tacticals-name-face)
-    (cons (proof-regexp-alt-list (list "Set" "Type" "Prop")) 'font-lock-type-face)
+    (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face)
     (cons "============================" 'font-lock-keyword-face)
     (cons "Subtree proved!" 'font-lock-keyword-face)
     (cons "subgoal [0-9]+ is:" 'font-lock-keyword-face)