aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-syntax.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2015-03-26 18:41:19 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2015-03-26 18:41:19 +0000
commit6a504a85265065b13c36cc56a807551044990b7c (patch)
tree807244c80d1263f8b8e20bbe942f7b9b81310f6f /coq/coq-syntax.el
parent2630829033e822158b3c89dd9d5e4f48ba92a026 (diff)
Colorizing hyps names robustified. Still incomplete.
Diffstat (limited to 'coq/coq-syntax.el')
-rw-r--r--coq/coq-syntax.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index c91ad2d9..99ee351b 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 "^ \\{0,2\\}\\([^\n :(),]\\|, \\)+ *:" 'proof-declaration-name-face)
(list "^\\([^ \n]+\\) \\(is defined\\)"
(list 1 'font-lock-function-name-face t)))))
@@ -1086,7 +1086,7 @@ It is used:
(append
coq-font-lock-terms
(list
- (cons "^ *\\([^ \n:()=]\\|, \\)+ *:" 'proof-declaration-name-face)
+ (cons "^ \\{0,2\\}\\([^ \n:()=]\\|, \\)+ *:" 'proof-declaration-name-face)
(cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face))))