aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-syntax.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2015-04-07 09:04:33 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2015-04-07 09:04:33 +0000
commitc2eb2fdc71728878b019c1b87ff8cdc5d96bb00c (patch)
treeeba603baf7fa0b44b293457c7180f41b3ccbca45 /coq/coq-syntax.el
parent7aaf6c9f278062ab6744aa036226a1c4be34d98b (diff)
Fixed highlighting of evars.
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 14ca9c48..33f5382e 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1076,7 +1076,7 @@ It is used:
(cons coq-error-regexp 'proof-error-face)
(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)
- (list "[?][a-zA-Z0-9]+" 0 'proof-eager-annotation-face);; highlight evars
+ (list (concat "[?]" proof-id) 0 'proof-eager-annotation-face);; highlight evars
;; ", " is for multiple hypothesis diplayed in v8.5.
(cons "^ \\{0,2\\}\\([^\n :(),]\\|, \\)+ *:" 'proof-declaration-name-face)
(list "^\\([^ \n]+\\) \\(is defined\\)" (list 1 'font-lock-function-name-face t)))))
@@ -1085,7 +1085,7 @@ It is used:
(append
coq-font-lock-terms
(list
- (list "[?][a-zA-Z0-9]+" 0 'proof-eager-annotation-face);; highlight evars
+ (list (concat "[?]" proof-id) 0 'proof-eager-annotation-face);; highlight evars
(cons "^ \\{0,2\\}\\([^ \n:()=]\\|, \\)+ *:" 'proof-declaration-name-face)
(cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face))))