*.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)|(Variant)|(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
under
without loss
wlog
by
over
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)