diff options
| author | Pierre-Marie Pédrot | 2016-06-05 21:50:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-15 20:21:37 +0200 |
| commit | dcf4d3e28813e09fc71f974b79ddf42d2e525976 (patch) | |
| tree | 76a95699918b818e3f6111b594b5b6ec7bd566b2 /ide | |
| parent | 4d239ab9f096843dc1c78744dfc9b316ab49d6d9 (diff) | |
Remove the syntax changes introduced by this branch.
We decided to only export the API, so that an external plugin can provide
this feature without having to merge it in current Coq trunk. This postpones
the attribute implementation in vernacular commands after 8.6.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.lang | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/ide/coq.lang b/ide/coq.lang index a31eadc707..c65432bdb7 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -29,13 +29,12 @@ <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex> <define-regex id="dot_sep">\.(\s|\z)</define-regex> <define-regex id="bullet">([-+*]+|{)(\s|\z)|}(\s*})*</define-regex> - <define-regex id="assume">(?'gal0'Assume)\%{space}\[\%{ident}*\]\%{space}</define-regex> <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|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> <define-regex id="end_proof">Qed|Defined|Admitted|Abort|Save</define-regex> - <define-regex id="decl_head">((\%{assume})?(?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal)</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})*))|(?'gal2'Goal)</define-regex> <!-- Strings, with '""' an escape sequence --> <context id="string" style-ref="string" class="string"> @@ -107,7 +106,6 @@ <end>\%{dot_sep}</end> <include> <context sub-pattern="id" where="start" style-ref="identifier"/> - <context sub-pattern="gal0" where="start" style-ref="gallina-keyword"/> <context sub-pattern="gal" where="start" style-ref="gallina-keyword"/> <context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/> <context sub-pattern="id_list" where="start" style-ref="identifier"/> |