diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-06 14:53:44 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-06 14:53:44 +0100 |
commit | d0801d05923278f3dd908c7965085cc052063944 (patch) | |
tree | 4615ebd27e48faec5b3b5c15f0f095d2861c2720 /ide/coq.lang | |
parent | 7dd73ff65ad78b20ff25170f33d15a06ac006ae2 (diff) |
Fix syntax highlighting of Hypothesis, Axiom, Variable, Parameter, and Context.
Diffstat (limited to 'ide/coq.lang')
-rw-r--r-- | ide/coq.lang | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/coq.lang b/ide/coq.lang index 733f1dcec..94ee77ae1 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -29,8 +29,8 @@ <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)|(Coercion)</define-regex> - <define-regex id="mult_decl">(Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)</define-regex> + <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Class)|(Module(\%{space}+Type)?)|(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> <define-regex id="end_proof">(Qed)|(Defined)|(Admitted)|(Abort)</define-regex> |