Specification language

match

in

type_scope

function_scope

Arguments

:=

Proofs

Proof using

Scheme

Derive

Inversion

omega

lra

lia

nra

nia

psatz

zify

nsatz

L

Using Coq

Functional

-vos

Appendix

+ (backtracking branching)

=>

[> … | … | … ] (dispatch)

abstract

abstract (ssreflect)

absurd

admit

apply

apply (ssreflect)

apply … in

apply … in … as

assert

assert_fails

assert_succeeds

assumption

auto

autoapply

autorewrite

autounfold

btauto

by

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

context

contradict

contradiction

convert_concl_no_check

cut

cutrewrite

cycle

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

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

eval

evar

exact

exact (ssreflect)

exact_no_check

exactly_once

exfalso

exists

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

generalize

generally have

gfail

give_up

guard

has_evar

have

hnf

idtac

induction

induction … using …

info_trivial

infoH

injection

instantiate

intro

intros

intros …

intuition

inversion

inversion ... using ...

inversion_clear

inversion_sigma

is_evar

is_var

lapply

last

last first

lazy

lazymatch

lazymatch goal

left

let

ltac-seq

match goal

move

move … after …

move … at bottom

move … at top

move … before …

multimatch

multimatch goal

native_cast_no_check

native_compute

notypeclasses refine

now

numgoals

once

only

optimize_heap

over

pattern

pose

pose (ssreflect)

pose proof

progress

rapply

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

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

tauto

time

time_constr

timeout

transitivity

transparent_abstract

trivial

try

tryif

type of

type_term

typeclasses eauto

under

unfold

unify

unlock

unshelve

vm_cast_no_check

vm_compute

with_strategy

without loss

wlog

|| (first tactic making progress)

… : … (goal selector)

… : … (ssreflect)