aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.lang
diff options
context:
space:
mode:
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>