diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2013-12-03 11:09:54 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2013-12-03 11:09:54 +0100 |
| commit | a0383d4ce6d69b086331310b32c7262223a659e5 (patch) | |
| tree | b9629546044f42266648fadd9360a54b3fe374cb | |
| parent | 1e5e934a8ce31c129368e57b61e485e6b989c3f4 (diff) | |
Ensure locality modifiers are properly highlighted in CoqIDE.
| -rw-r--r-- | ide/coq.lang | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coq.lang b/ide/coq.lang index 718eb718f..b6f081521 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -34,7 +34,7 @@ <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> - <define-regex id="decl_head">((?'gal'(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))</define-regex> + <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))</define-regex> <context id="escape-seq" style-ref="escape"> <match>""</match> |