aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGuillaume Melquiond2015-03-06 15:08:31 +0100
committerGuillaume Melquiond2015-03-06 15:08:31 +0100
commit560e06e3409003bb58b158cf5f156eb3db70c227 (patch)
tree90cea83be52104f38445cb7f8ccc4074298e62d0
parentf3fdaff32e20c1a05defd2670cffaa3eee752eaf (diff)
Do not highlight "using" as a constr keyword.
-rw-r--r--ide/coq.lang1
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/coq.lang b/ide/coq.lang
index 46d91816a7..09b59d4625 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -97,7 +97,6 @@
<keyword>then</keyword>
<keyword>else</keyword>
<keyword>return</keyword>
- <keyword>using</keyword>
</context>
<context id="constr-sort" style-ref="constr-sort">
<keyword>Prop</keyword>