aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2007-11-07 10:59:30 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2007-11-07 10:59:30 +0000
commit6f8ade23551add38a07a62033993f85f4efe3872 (patch)
treeaecf1dd430987f96c958b538511521c8f085161c /coq
parent86ae89e6fff296ae7972c0e806e7f94c9097748c (diff)
Debugging font-lock regexp.
Diffstat (limited to 'coq')
-rw-r--r--coq/coq-syntax.el7
1 files changed, 2 insertions, 5 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 86b00f24..8e84b18d 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -813,9 +813,6 @@ Used by `coq-goal-command-p'"
(defvar coq-ids (proof-ids coq-id " "))
-(defun coq-first-abstr-regexp (paren)
- (concat paren "\\s-*\\(" coq-ids "\\)\\s-*:[^:]")) ; [^: to avoid color on (x::l)]
-
(defun coq-first-abstr-regexp (paren end)
(concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end))
@@ -827,9 +824,9 @@ Used by `coq-goal-command-p'"
(defvar coq-font-lock-terms
(list
;; lambda binders
- (list (coq-first-abstr-regexp "fun\>" "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face)
+ (list (coq-first-abstr-regexp "\\<fun\\>" "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face)
;; forall binder
- (list (coq-first-abstr-regexp "forall\>" "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face)
+ (list (coq-first-abstr-regexp "\\<forall\\>" "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face)
;; Pi binders
(list (coq-first-abstr-regexp "(" ":[^:=]") 1 'font-lock-variable-name-face)
;; second, third, etc. abstraction for Lambda of Pi binders