aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.lang
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-03-06 14:46:04 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-03-06 14:46:04 +0100
commit7dd73ff65ad78b20ff25170f33d15a06ac006ae2 (patch)
tree724109aed80683d96ff100a82af577024d97fb15 /ide/coq.lang
parent3e28afcde1e1c6423c0d2ef9d88094cbd9c5a68c (diff)
Add syntax highlighting for Coercion.
Diffstat (limited to 'ide/coq.lang')
-rw-r--r--ide/coq.lang2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coq.lang b/ide/coq.lang
index 6f7994fae..733f1dcec 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -29,7 +29,7 @@
<define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex>
<define-regex id="undotted_sep">[-+*{}]</define-regex>
<define-regex id="dot_sep">\.(\s|\z)</define-regex>
- <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)</define-regex>
+ <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Coercion)</define-regex>
<define-regex id="mult_decl">(Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)</define-regex>
<define-regex id="locality">(((Local)|(Global))\%{space}+)?</define-regex>
<define-regex id="begin_proof">(Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)</define-regex>