diff options
| author | Guillaume Melquiond | 2015-03-06 16:07:52 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-03-06 16:07:52 +0100 |
| commit | bdfed9edf1e7ed929d1867442587c6ecef30986b (patch) | |
| tree | 1c967bb49783452e9e3c197957e84bac2cabda62 | |
| parent | b4abf41dc6a6b2c6471185d6c102dbe1460a32cd (diff) | |
Fix syntax highlighting of Module (Type).
| -rw-r--r-- | ide/coq.lang | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/coq.lang b/ide/coq.lang index 1622e13330..2242ef1022 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)|(Function)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Coercion)</define-regex> + <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Function)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Class)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Coercion)</define-regex> <define-regex id="mult_decl">(Hypothes[ie]s)|(Axiom(s)?)|(Variable(s)?)|(Parameter(s)?)|(Context)|(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> @@ -190,6 +190,7 @@ <keyword>Scheme\%{space}((Induction)|(Minimality)|(Elimination)|(Case)|(Equality))\%{space}for</keyword> <keyword>End</keyword> <keyword>Section</keyword> + <keyword>Module(\%{space}+Type)?</keyword> <keyword>Declare\%{space}+Module(\%{space}+((Import)|(Export)))?</keyword> <keyword>About</keyword> <keyword>Arguments</keyword> |
