<?xml version="1.0" encoding="UTF-8"?>
<language id="coq" _name="Coq" version="2.0" _section="Scientific">
<metadata>
<property name="globs">*.v</property>
<property name="block-comment-start">\(\*</property>
<property name="block-comment-stop">\*\)</property>
</metadata>
<styles>
<style id="comment" _name="Comment" map-to="def:comment"/>
<style id="coqdoc" _name="Coqdoc text" map-to="def:note"/>
<style id="vernac-keyword" _name="Vernacular keyword" map-to="def:keyword"/>
<style id="gallina-keyword" _name="Gallina keyword" map-to="def:keyword"/>
<style id="identifier" _name="Identifier" map-to="def:identifier"/>
<style id="constr-keyword" _name="Cic keyword" map-to="def:keyword"/>
<style id="constr-sort" _name="Cic sort" map-to="def:builtin"/>
<style id="string" _name="String" map-to="def:string"/>
<style id="escape" _name="Escaped Character" map-to="def:special-char"/>
<style id="error" _name="Error" map-to="def:error"/>
<style id="safe" _name="Checked Part"/>
<style id="sentence" _name="Sentence terminator"/>
</styles>
<definitions>
<define-regex id="space">\s+</define-regex>
<define-regex id="first_ident_char">[_\p{L}]</define-regex>
<define-regex id="ident_char">[_\p{L}'\pN]</define-regex>
<define-regex id="ident">\%{first_ident_char}\%{ident_char}*</define-regex>
<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="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion|Universe</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">((?'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">
<start>"</start>
<end>"</end>
<include>
<context id="string-escape" style-ref="escape">
<match>""</match>
</context>
</include>
</context>
<!-- Coqdoc comments -->
<context id="coqdoc" style-ref="coqdoc" class="comment" class-disabled="no-spell-check">
<start>\(\*\*(\s|\z)</start>
<end>\*\)</end>
<include>
<context ref="comment"/>
<context ref="string"/>
<context ref="def:in-comment"/>
</include>
</context>
<!-- Regular comments, possibly nested -->
<context id="comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
<start>\(\*</start>
<end>\*\)</end>
<include>
<context ref="comment"/>
<context ref="string"/>
<context ref="def:in-comment"/>
</include>
</context>
<!-- Keywords for constr -->
<context id="constr-keyword" style-ref="constr-keyword">
<keyword>forall</keyword>
<keyword>fun</keyword>
<keyword>match</keyword>
<keyword>fix</keyword>
<keyword>cofix</keyword>
<keyword>with</keyword>
<keyword>for</keyword>
<keyword>end</keyword>
<keyword>as</keyword>
<keyword>let</keyword>
<keyword>in</keyword>
<keyword>if</keyword>
<keyword>then</keyword>
<keyword>else</keyword>
<keyword>return</keyword>
</context>
<!-- Sort keywords -->
<context id="constr-sort" style-ref="constr-sort">
<keyword>Prop</keyword>
<keyword>Set</keyword>
<keyword>Type</keyword>
</context>
<!-- Terms -->
<context id="constr">
<include>
<context ref="string"/>
<context ref="coqdoc"/>
<context ref="comment"/>
<context ref="constr-sort"/>
<context ref="constr-keyword"/>
<context id="dot-nosep">
<match>\.\.</match>
</context>
</include>
</context>
<context id="coq" class="no-spell-check">
<include>
<context ref="coqdoc"/>
<context ref="comment"/>
<context id="declaration">
<start>\%{decl_head}</start>
<end>\%{dot_sep}</end>
<include>
<context sub-pattern="id" where="start" style-ref="identifier"/>
<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"/>
<context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/>
<context ref="constr"/>
</include>
</context>
<context id="proof">
<start>(Proof(\%{dot_sep}|\%{space}using|\%{space}with))|Next Obligation</start>
<end>\%{end_proof}\%{dot_sep}</end>
<include>
<context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
<context sub-pattern="0" where="end" style-ref="vernac-keyword"/>
<context ref="coqdoc"/>
<context ref="comment"/>
<context id="bullet" style-ref="vernac-keyword" extend-parent="false">
<match>\%{bullet}</match>
</context>
<context extend-parent="false">
<start>\%[</start>
<end>\%{dot_sep}</end>
<include>
<context ref="command-in-proof"/>
<context ref="constr"/>
</include>
</context>
</include>
</context>
<context id="exact-proof">
<start>Proof</start>
<end>\%{dot_sep}</end>
<include>
<context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
<context ref="constr"/>
</include>
</context>
<context ref="command"/>
</include>
</context>
<!-- Toplevel commands -->
<context id="command" extend-parent="false">
<start>\%[</start>
<end>\%{dot_sep}</end>
<include>
<context id="command-in-proof" style-ref="vernac-keyword">
<keyword>About</keyword>
<keyword>Check</keyword>
<keyword>Print</keyword>
<keyword>Eval</keyword>
<keyword>Undo</keyword>
<keyword>Restart</keyword>
<keyword>Opaque</keyword>
<keyword>Transparent</keyword>
</context>
<context id="toplevel-command" style-ref="vernac-keyword">
<keyword>Add</keyword>
<keyword>Load</keyword>
<keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword>
<keyword>Comments</keyword>
<keyword>Solve\%{space}Obligation</keyword>
<keyword>(Uns|S)et(\%{space}\%{ident})+</keyword>
<keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword>
<keyword>\%{locality}Infix</keyword>
<keyword>Declare\%{space}ML\%{space}Module</keyword>
<keyword>Extraction\%{space}Language\%{space}(OCaml|Haskell|Scheme|JSON)</keyword>
</context>
<context id="hint-command" style-ref="vernac-keyword">
<prefix>\%{locality}Hint\%{space}</prefix>
<keyword>Resolve</keyword>
<keyword>Immediate</keyword>
<keyword>Constructors</keyword>
<keyword>Unfold</keyword>
<keyword>Extern</keyword>
<keyword>Rewrite</keyword>
</context>
<context id="scope-command" style-ref="vernac-keyword">
<suffix>\%{space}Scope</suffix>
<keyword>\%{locality}Open</keyword>
<keyword>\%{locality}Close</keyword>
<keyword>Bind</keyword>
<keyword>Delimit</keyword>
</context>
<context id="command-for-qualit">
<suffix>\%{space}(?'qua'\%{qualit})</suffix>
<keyword>Chapter</keyword>
<keyword>Combined\%{space}Scheme</keyword>
<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>Arguments</keyword>
<keyword>Implicit\%{space}Arguments</keyword>
<keyword>Include</keyword>
<keyword>Extract\%{space}((Inlined\%{space})?Constant|Inductive)</keyword>
<include>
<context sub-pattern="1" style-ref="vernac-keyword"/>
<context sub-pattern="qua" style-ref="identifier"/>
</include>
</context>
<context id="command-for-qualit-list">
<suffix>(?'qua_list'(\%{space}\%{qualit})+)</suffix>
<keyword>Typeclasses (Transparent|Opaque)</keyword>
<keyword>Require(\%{space}(Import|Export))?</keyword>
<keyword>Import</keyword>
<keyword>Export</keyword>
<keyword>((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))?</keyword>
<include>
<context sub-pattern="1" style-ref="vernac-keyword"/>
<context sub-pattern="qua_list" style-ref="identifier"/>
</include>
</context>
<context ref="constr"/>
</include>
</context>
</definitions>
</language>
