diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-09-22 10:48:51 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-09-22 10:48:51 +0200 |
| commit | f0c74c416cd356ed1261e25bc70e60551acb28f9 (patch) | |
| tree | a3263759b7a07f65eb117aaa2149fc889ca3bef2 /coq/coq-syntax.el | |
| parent | 6444de9025c84c443427c0bddc2af7335da77b59 (diff) | |
hyps highlighting now supports compact contexts (in coq trunk soon).
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 17fcd97d..e86d1fc9 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1093,7 +1093,7 @@ It is used: (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face) (list (concat "[?]" coq-id) 0 'proof-eager-annotation-face);; highlight evars ;; ", " is for multiple hypothesis diplayed in v8.5. - (cons "^ \\{0,2\\}\\([^\n :(),]\\|, \\)+ *:" 'proof-declaration-name-face) + (cons "^ \\{0,1,2\\}\\([^\n :(),]\\|, \\)+ *:" 'proof-declaration-name-face) (list "^\\([^ \n]+\\) \\(is defined\\)" (list 1 'font-lock-function-name-face t))))) (defvar coq-goals-font-lock-keywords @@ -1102,7 +1102,7 @@ It is used: (list (cons coq-reserved-regexp 'font-lock-type-face) (list (concat "[?]" coq-id) 0 'proof-eager-annotation-face);; highlight evars - (cons "^ \\{0,2\\}\\([^ \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)))) |