|
|
- # 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
|
