aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.lang
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-03-06 16:03:40 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-03-06 16:03:40 +0100
commit5743fd25fa058e4cf7b5949b8287935163de9232 (patch)
treec85e6c004ae681053c4aeb6f651972a0e812074b /ide/coq.lang
parentc1587dfec7ecbd48e2404d8c4744eacfce08a943 (diff)
Add syntax highlighting for Declare ML Module.
Diffstat (limited to 'ide/coq.lang')
-rw-r--r--ide/coq.lang1
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/coq.lang b/ide/coq.lang
index 43268b0c3..1842f7942 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -163,6 +163,7 @@
<keyword>(\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation</keyword>
<keyword>\%{locality}Infix</keyword>
<keyword>(Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist)</keyword>
+ <keyword>Declare\%{space}+ML\%{space}+Module</keyword>
</context>
<context id="hint-command" style-ref="vernac-keyword">
<prefix>\%{locality}Hint\%{space}+</prefix>