aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-09-17 16:28:50 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-09-17 16:28:50 +0200
commita66d6e8e6d52d156d52e6282b879347c8922a4e8 (patch)
tree0ba597ff4d04c903791818cd3352a1bc67365bef /ide
parent230b1e9304afce6be810bcc333ad756e5d0d885a (diff)
Fix highlighting of "Hint Unfold" and "Hint Rewrite".
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.lang3
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/coq.lang b/ide/coq.lang
index d791eadc7..7679f863d 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -174,10 +174,11 @@
<keyword>Resolve</keyword>
<keyword>Immediate</keyword>
<keyword>Constructors</keyword>
- <keyword>unfold</keyword>
+ <keyword>Unfold</keyword>
<keyword>Opaque</keyword>
<keyword>Transparent</keyword>
<keyword>Extern</keyword>
+ <keyword>Rewrite</keyword>
</context>
<context id="scope-command" style-ref="vernac-keyword">
<suffix>\%{space}+Scope</suffix>