*.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)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Canonical)|(Coercion)
(Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)
(((Local)|(Global))\%{space}+)?
(Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)
(Qed)|(Defined)|(Admitted)|(Abort)
((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))
""
"
"
do
last
first
apply
auto
case
case
congr
elim
exists
have
gen have
generally have
move
pose
rewrite
set
split
suffices
suff
transitivity
without loss
wlog
by
exact
reflexivity
\(\*\*(\s|\z)
\*\)
\%{decl_head}
\%{dot_sep}
forall
fun
match
fix
cofix
with
for
end
as
let
in
if
then
else
return
using
Prop
Set
Type
\.\.
Proof
\%{end_proof}\%{dot_sep}
\%{dot_sep}
\%{undotted_sep}
Add
Check
Eval
Load
Undo
Restart
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
Implicit\%{space}+Arguments
(Import)|(Include)
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)