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)
 
.
... : ... (goal selector)
... : ... (ssreflect)
 
=
=>
 
[
[> ... | ... | ... ] (dispatch)
 
_
_
 
a
abstract
abstract (ssreflect)
absurd
admit
all: ...
apply
apply (ssreflect)
apply ... in
apply ... in ... as
assert
assert_fails
assert_succeeds
assumption
auto
autoapply
autorewrite
autounfold
 
b
btauto
by
 
c
case
case (ssreflect)
cbn
cbv
change
change_no_check
classical_left
classical_right
clear
clearbody
cofix
compare
compute
congr
congruence
congruence with
constr_eq
constr_eq_strict
constructor
contradict
contradiction
convert_concl_no_check
cut
cutrewrite
cycle
 
d
debug auto
debug trivial
decide equality
decompose
dependent destruction
dependent induction
dependent inversion
dependent inversion ... with ...
dependent rewrite ->
dependent rewrite <-
destruct
destruct ... eqn:
dintuition
discriminate
discrR
do
do (ssreflect)
done
double induction
dtauto
 
e
eapply
eassert
eassumption
easy
eauto
ecase
econstructor
edestruct
ediscriminate
eelim
eenough
eexact
eexists
einduction
einjection
eintros
eleft
elim
elim (ssreflect)
elim ... with
elimtype
enough
epose
epose proof
eremember
erewrite
eright
eset
esimplify_eq
esplit
evar
exact
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
function induction
functional inversion
 
g
generalize
generally have
gfail
give_up
guard
 
h
has_evar
have
hnf
 
i
idtac
in
induction
induction ... using ...
info_trivial
injection
instantiate
intro
intros
intros ...
intuition
inversion
inversion ... using ...
inversion_clear
inversion_sigma
is_evar
is_var
 
l
lapply
last
last first
lazy
left
let ... := ...
lia
lra
ltac-seq
 
m
match goal
move
move ... after ...
move ... at bottom
move ... at top
move ... before ...
 
n
native_cast_no_check
native_compute
nia
notypeclasses refine
now
nra
nsatz
 
o
omega
once
only ... : ...
optimize_heap
over
 
p
par: ...
pattern
pose
pose (ssreflect)
pose proof
progress
psatz
 
r
red
refine
reflexivity
remember
rename
repeat
replace
reset ltac profile
restart_timer
revert
revert dependent
revgoals
rewrite
rewrite (ssreflect)
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 destruct
simple eapply
simple induction
simple inversion
simple notypeclasses refine
simple refine
simplify_eq
solve
solve_constraints
specialize
split
split_Rabs
split_Rmult
start ltac profiling
stepl
stepr
stop ltac profiling
subst
suff
suffices
swap
symmetry
 
t
tauto
time
time_constr
timeout
transitivity
transparent_abstract
trivial
try
tryif
typeclasses eauto
 
u
under
unfold
unify
unlock
unshelve
 
v
vm_cast_no_check
vm_compute
 
w
without loss
wlog
 
z
zify
 
|
|| (left-biased branching)