279 lines
2.5 KiB
Plaintext
279 lines
2.5 KiB
Plaintext
# Generated by the following form.
|
|
# (loop for regexp in (append
|
|
# coq-solve-tactics
|
|
# coq-keywords
|
|
# coq-reserved
|
|
# coq-tactics
|
|
# coq-tacticals
|
|
# (list "Set" "Type" "Prop"))
|
|
# append (split-string regexp (regexp-quote "\\s-+")) into words
|
|
# finally (loop initially (goto-char (point-max))
|
|
# for word in (delete-dups (sort words 'string<))
|
|
# do (insert word) (newline)))
|
|
|
|
Abort
|
|
About
|
|
Abstract
|
|
Add
|
|
Admit
|
|
Admitted
|
|
All
|
|
Arguments
|
|
AutoInline
|
|
Axiom
|
|
Bind
|
|
Canonical
|
|
Cd
|
|
Chapter
|
|
Check
|
|
Close
|
|
CoFixpoint
|
|
CoInductive
|
|
Coercion
|
|
Coercions
|
|
Comments
|
|
Conjecture
|
|
Constant
|
|
Constructors
|
|
Corollary
|
|
Declare
|
|
Defined
|
|
Definition
|
|
Delimit
|
|
Dependent
|
|
Depth
|
|
Derive
|
|
End
|
|
Eval
|
|
Export
|
|
Extern
|
|
Extract
|
|
Extraction
|
|
Fact
|
|
False
|
|
Field
|
|
File
|
|
Fixpoint
|
|
Focus
|
|
Function
|
|
Functional
|
|
Goal
|
|
Hint
|
|
Hypotheses
|
|
Hypothesis
|
|
Hyps
|
|
Identity
|
|
If
|
|
Immediate
|
|
Implicit
|
|
Import
|
|
Inductive
|
|
Infix
|
|
Inline
|
|
Inlined
|
|
Inspect
|
|
Inversion
|
|
Language
|
|
Lemma
|
|
Let
|
|
Library
|
|
Limit
|
|
LoadPath
|
|
Local
|
|
Locate
|
|
Ltac
|
|
ML
|
|
Module
|
|
Morphism
|
|
Next Obligation
|
|
NoInline
|
|
Notation
|
|
Notations
|
|
Obligation
|
|
Obligations
|
|
Off
|
|
On
|
|
Opaque
|
|
Open
|
|
Optimize
|
|
Parameter
|
|
Parameters
|
|
Path
|
|
Print
|
|
Printing
|
|
Program
|
|
Proof
|
|
Prop
|
|
Pwd
|
|
Qed
|
|
Rec
|
|
Record
|
|
Recursive
|
|
Remark
|
|
Remove
|
|
Require
|
|
Reserved
|
|
Reset
|
|
Resolve
|
|
Rewrite
|
|
Ring
|
|
Save
|
|
Scheme
|
|
Scope
|
|
Search
|
|
SearchAbout
|
|
SearchPattern
|
|
SearchRewrite
|
|
Section
|
|
Semi
|
|
Set
|
|
Setoid
|
|
Show
|
|
Solve
|
|
Sort
|
|
Strict
|
|
Structure
|
|
Synth
|
|
Tactic
|
|
Test
|
|
Theorem
|
|
Time
|
|
Transparent
|
|
True
|
|
Type
|
|
Undo
|
|
Unfocus
|
|
Unfold
|
|
Unset
|
|
Variable
|
|
Variables
|
|
Width
|
|
Wildcard
|
|
abstract
|
|
absurd
|
|
after
|
|
apply
|
|
as
|
|
assert
|
|
assumption
|
|
at
|
|
auto
|
|
autorewrite
|
|
beta
|
|
by
|
|
case
|
|
cbv
|
|
change
|
|
clear
|
|
clearbody
|
|
cofix
|
|
coinduction
|
|
compare
|
|
compute
|
|
congruence
|
|
constructor
|
|
contradiction
|
|
cut
|
|
cutrewrite
|
|
decide
|
|
decompose
|
|
delta
|
|
dependent
|
|
dest
|
|
destruct
|
|
discrR
|
|
discriminate
|
|
do
|
|
double
|
|
eapply
|
|
eauto
|
|
econstructor
|
|
eexists
|
|
eleft
|
|
elim
|
|
else
|
|
end
|
|
equality
|
|
esplit
|
|
exact
|
|
exists
|
|
fail
|
|
field
|
|
first
|
|
firstorder
|
|
fix
|
|
fold
|
|
forall
|
|
fourier
|
|
fun
|
|
functional
|
|
generalize
|
|
hnf
|
|
idtac
|
|
if
|
|
in
|
|
induction
|
|
info
|
|
injection
|
|
instantiate
|
|
into
|
|
intro
|
|
intros
|
|
intuition
|
|
inversion
|
|
inversion_clear
|
|
iota
|
|
lapply
|
|
lazy
|
|
left
|
|
let
|
|
linear
|
|
load
|
|
match
|
|
move
|
|
omega
|
|
pattern
|
|
pose
|
|
progress
|
|
prolog
|
|
quote
|
|
record
|
|
red
|
|
refine
|
|
reflexivity
|
|
rename
|
|
repeat
|
|
replace
|
|
return
|
|
rewrite
|
|
right
|
|
ring
|
|
set
|
|
setoid
|
|
setoid_replace
|
|
setoid_rewrite
|
|
simpl
|
|
simple
|
|
simplify_eq
|
|
solve
|
|
specialize
|
|
split
|
|
split_Rabs
|
|
split_Rmult
|
|
stepl
|
|
stepr
|
|
struct
|
|
subst
|
|
sum
|
|
symmetry
|
|
tauto
|
|
then
|
|
transitivity
|
|
trivial
|
|
try
|
|
unfold
|
|
until
|
|
using
|
|
with
|
|
zeta
|