*.v
\(\*
\*\)
\s+
[_\p{L}]
[_\p{L}'\pN]
\%{first_ident_char}\%{ident_char}*
(\%{ident}\.)*\%{ident}
\.(\s|\z)
([-+*]+|{)(\s|\z)|}(\s*})*
Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion|Universe
Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?
((Local|Global)\%{space})?
Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property
Qed|Defined|Admitted|Abort|Save
((?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal)
"
"
""
forall
fun
match
fix
cofix
with
for
end
as
let
in
if
then
else
return
Prop
Set
Type
\%{decl_head}
\%{dot_sep}
\.\.
(Proof(\%{dot_sep}|\%{space}using|\%{space}with))|Next Obligation
\%{end_proof}\%{dot_sep}
\%{dot_sep}\s*(?'bul'\%{bullet})
^\s*\%{bullet}
Proof
\%{dot_sep}
About
Check
Print
Eval
Undo
Restart
Opaque
Transparent
Add
Load
(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)
Comments
Solve\%{space}Obligation
(Uns|S)et(\%{space}\%{ident})+
(\%{locality}|(Reserved|Tactic)\%{space})?Notation
\%{locality}Infix
Declare\%{space}ML\%{space}Module
Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)
\%{locality}Hint\%{space}
Resolve
Immediate
Constructors
Unfold
Extern
Rewrite
\%{space}Scope
\%{locality}Open
\%{locality}Close
Bind
Delimit
\%{space}(?'qua'\%{qualit})
Chapter
Combined\%{space}Scheme
Scheme\%{space}(Induction|Minimality|Elimination|Case|Equality)\%{space}for
End
Section
Module(\%{space}Type)?
Declare\%{space}Module(\%{space}(Import|Export))?
Arguments
Implicit\%{space}Arguments
Include
Extract\%{space}((Inlined\%{space})?Constant|Inductive)
(?'qua_list'(\%{space}\%{qualit})+)
Typeclasses (Transparent|Opaque)
Require(\%{space}(Import|Export))?
Import
Export
((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))?