aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-syntax.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2015-03-26 16:20:30 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2015-03-26 16:20:30 +0000
commitf9663fdac4e0204b535abb9a6ff509e5717a82a0 (patch)
tree1736dfbe78ab4b0e3e73144400b3dca0117bf9b0 /coq/coq-syntax.el
parent3f206f8658bd5fabe6726a39c0fa0c9405fcca8d (diff)
Fixed a smal bug in colorizing response buffer.
First constructor of an inductive was colorized as a hyp name. Hyp name colorizing should be done another way. Using font-lock here is probably bad.
Diffstat (limited to 'coq/coq-syntax.el')
-rw-r--r--coq/coq-syntax.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 0fd200f5..c91ad2d9 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1078,7 +1078,7 @@ It is used:
(cons (proof-regexp-alt-list-symb (list "In environment" "The term" "has type")) 'proof-error-face)
(cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face)
;; ", " is for multiple hypothesis diplayed in v8.5.
- (cons "^ *\\([^\n :(),]\\|, \\)+ *:" 'proof-declaration-name-face)
+ (cons "^ \\([^\n :(),]\\|, \\)+ *:" 'proof-declaration-name-face)
(list "^\\([^ \n]+\\) \\(is defined\\)"
(list 1 'font-lock-function-name-face t)))))