aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.lang
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-03-06 16:51:10 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-03-06 16:51:10 +0100
commit0e9ad65b7302ae8fe419726e4a311e42e2dae749 (patch)
treee29312ce0859e0fd441af6c9c8357e1a654191e1 /ide/coq.lang
parent29268d7e8e3c9925515c1e7aaaa77ae535e7f46e (diff)
Fix syntax highlighting of Extraction Language.
Diffstat (limited to 'ide/coq.lang')
-rw-r--r--ide/coq.lang3
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/coq.lang b/ide/coq.lang
index cfacd7ca4..fee84bd32 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -164,6 +164,7 @@
<keyword>\%{locality}Infix</keyword>
<keyword>(Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist)</keyword>
<keyword>Declare\%{space}+ML\%{space}+Module</keyword>
+ <keyword>Extraction\%{space}+Language\%{space}+(Ocaml|Haskell|Scheme)</keyword>
</context>
<context id="hint-command" style-ref="vernac-keyword">
<prefix>\%{locality}Hint\%{space}+</prefix>
@@ -196,7 +197,7 @@
<keyword>Arguments</keyword>
<keyword>Implicit\%{space}+Arguments</keyword>
<keyword>Include</keyword>
- <keyword>(Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))?</keyword>
+ <keyword>(Recursive\%{space}+)?Extraction(\%{space}+((Library)|((No)?Inline)|(Blacklist)))?</keyword>
<keyword>Extract\%{space}+((Inlined\%{space}+)?(Constant)|(Inductive))</keyword>
<include>
<context sub-pattern="1" style-ref="vernac-keyword"/>