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