aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-syntax.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2015-03-27 10:14:32 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2015-03-27 10:14:32 +0000
commitfe158afe291c2ad5786bc592fff134ef277ef86d (patch)
treee3cc647956217875ebd51213c10207d53b710d64 /coq/coq-syntax.el
parent9d6766d2f20362240ebfe284e0dbd97fb25504a0 (diff)
Fix disable evar colorizing in coq file.
Diffstat (limited to 'coq/coq-syntax.el')
-rw-r--r--coq/coq-syntax.el6
1 files changed, 3 insertions, 3 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 99ee351b..14ca9c48 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -978,7 +978,6 @@ It is used:
; (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil
; (list 0 font-lock-variable-name-face)))
- (list "[?][a-zA-Z0-9]+" 0 'proof-eager-annotation-face)
;; parenthesized binders
(list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face)
(list (coq-first-abstr-regexp "{" ":[ a-zA-Z]") 1 'font-lock-variable-name-face)
@@ -1077,15 +1076,16 @@ 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
;; ", " 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)))))
+ (list "^\\([^ \n]+\\) \\(is defined\\)" (list 1 'font-lock-function-name-face t)))))
(defvar coq-goals-font-lock-keywords
(append
coq-font-lock-terms
(list
+ (list "[?][a-zA-Z0-9]+" 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))))