diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2015-03-27 10:14:32 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2015-03-27 10:14:32 +0000 |
| commit | fe158afe291c2ad5786bc592fff134ef277ef86d (patch) | |
| tree | e3cc647956217875ebd51213c10207d53b710d64 /coq/coq-syntax.el | |
| parent | 9d6766d2f20362240ebfe284e0dbd97fb25504a0 (diff) | |
Fix disable evar colorizing in coq file.
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 6 |
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)))) |