Tactic Index

+ | = | [ | a | b | c | d | e | f | g | h | i | l | m | n | o | p | r | s | t | u | v | w | x | 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`
	`autounfold_one`

	b
	`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_nounivs`
	`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_clear`
	`dependent rewrite`
	`dependent simple inversion`
	`destruct`
	`dfs eauto`
	`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_lookup`
	`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`
	`gintuition`
	`give_up`
	`guard`

	h
	`has_evar`
	`have`
	`hnf`

	i
	`idtac`
	`if-then-else (Ltac2)`
	`in`
	`induction`
	`info_auto`
	`info_eauto`
	`info_trivial`
	`injection`
	`instantiate`
	`intro`
	`intros`
	`intros …`
	`intuition`
	`inversion`
	`inversion_clear`
	`inversion_sigma`
	`is_cofix`
	`is_const`
	`is_constructor`
	`is_evar`
	`is_fix`
	`is_ground`
	`is_ind`
	`is_proj`
	`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`
	`nsatz_compute`
	`numgoals`

	o
	`once`
	`only`
	`optimize_heap`
	`over`

	p
	`pattern`
	`pose`
	`pose (ssreflect)`
	`pose proof`
	`progress`
	`protect_fv`
	`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_lookup`
	`ring_simplify`
	`rtauto`

	s
	`set`
	`set (ssreflect)`
	`setoid_etransitivity`
	`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 injection`
	`simple inversion`
	`simple notypeclasses refine`
	`simple refine`
	`simple subst`
	`simplify_eq`
	`soft functional induction`
	`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`
	`wlia`
	`wlog`
	`wlra_Q`
	`wnia`
	`wnra_Q`
	`wpsatz_Q`
	`wpsatz_Z`
	`wsos_Q`
	`wsos_Z`

	x
	`xlia`
	`xlra_Q`
	`xlra_R`
	`xnia`
	`xnra_Q`
	`xnra_R`
	`xpsatz_Q`
	`xpsatz_R`
	`xpsatz_Z`
	`xsos_Q`
	`xsos_R`
	`xsos_Z`

	z
	`zify`
	`zify_elim_let`
	`zify_iter_let`
	`zify_iter_specs`
	`zify_op`
	`zify_saturate`

	{
	`{`

	\|
	`\|\| (first tactic making progress)`

	}
	`}`

	…
	`… : … (goal selector)`
	`… : … (ssreflect)`