Tactic Index

+ | = | [ | a | b | c | d | e | f | g | h | i | l | m | n | o | p | r | s | t | u | v | w | z | { | | | } |
 
+
+ (backtracking branching)
 
=
=>
 
[
[ … | … | … ] (dispatch)
[> … | … | … ] (dispatch)
 
a
abstract
abstract (ssreflect)
absurd
admit
apply
apply (ssreflect)
apply … in
apply … in … as
assert
assert_fails
assert_succeeds
assumption
auto
autoapply
autorewrite
autounfold
 
b
bfs eauto
btauto
by
 
c
case
case (ssreflect)
case_eq
casetype
cbn
cbv
change
change_no_check
classical_left
classical_right
clear
clearbody
cofix
compare
compute
congr
congruence
constr_eq
constr_eq_strict
constructor
context
contradict
contradiction
cut
cutrewrite
cycle
 
d
debug auto
debug eauto
debug trivial
decide equality
decompose
dependent destruction
dependent induction
dependent inversion
dependent inversion … with …
dependent rewrite ->
dependent rewrite <-
destruct
dintuition
discriminate
discrR
do
do (ssreflect)
done
dtauto
 
e
eapply
eassert
eassumption
easy
eauto
ecase
econstructor
edestruct
ediscriminate
eelim
eenough
eexact
eexists
einduction
einjection
eintros
eleft
elim
elim (ssreflect)
elimtype
enough
epose
epose proof
eremember
erewrite
eright
eset
esimplify_eq
esplit
etransitivity
eval
evar
exact
exact (ssreflect)
exact_no_check
exactly_once
exfalso
exists
 
f
f_equal
fail
field
field_simplify
field_simplify_eq
finish_timing
first
first (ssreflect)
first last
firstorder
fix
fold
fresh
fun
functional induction
functional inversion
 
g
generalize
generally have
gfail
give_up
guard
 
h
has_evar
have
hnf
 
i
idtac
if-then-else (Ltac2)
in
induction
info_auto
info_eauto
info_trivial
infoH
injection
instantiate
intro
intros
intros …
intuition
inversion
inversion ... using ...
inversion_clear
inversion_sigma
is_evar
is_var
 
l
lapply
last
last first
lazy
lazy_match!
lazy_match! goal
lazymatch
lazymatch goal
left
let
lia
lra
ltac-seq
 
m
match
match (Ltac2)
match goal
match!
match! goal
move
move (ssreflect)
move … at bottom
move … at top
move … before …
multi_match!
multi_match! goal
multimatch
multimatch goal
 
n
native_cast_no_check
native_compute
nia
notypeclasses refine
now
now_show
nra
nsatz
numgoals
 
o
once
only
optimize_heap
over
 
p
pattern
pose
pose (ssreflect)
pose proof
progress
psatz
 
r
rapply
red
refine
reflexivity
remember
rename
repeat
replace
reset ltac profile
restart_timer
revert
revert dependent
revgoals
rewrite
rewrite (ssreflect)
rewrite *
rewrite_db
rewrite_strat
right
ring
ring_simplify
rtauto
 
s
set
set (ssreflect)
setoid_reflexivity
setoid_replace
setoid_rewrite
setoid_symmetry
setoid_transitivity
shelve
shelve_unifiable
show ltac profile
simpl
simple apply
simple congruence
simple destruct
simple eapply
simple induction
simple inversion
simple notypeclasses refine
simple refine
simple subst
simplify_eq
solve
solve_constraints
specialize
split
split_Rabs
split_Rmult
start ltac profiling
stepl
stepr
stop ltac profiling
subst
substitute
suff
suffices
swap
symmetry
 
t
tauto
time
time_constr
timeout
transitivity
transparent_abstract
trivial
try
tryif
type of
type_term
typeclasses eauto
 
u
under
unfold
unify
unlock
unshelve
 
v
vm_cast_no_check
vm_compute
 
w
with_strategy
without loss
wlog
 
z
zify
 
{
{
 
|
|| (first tactic making progress)
 
}
}
 
… : … (goal selector)
… : … (ssreflect)