# Coq Reference Manual

# Global Index

- ∣∣, 9.2
- *, 3.1.3, 3.2.2
- +, 3.1.3, 3.2.2
- -, 3.2.2
- /, 3.2.2
- 2-level approach, 8.10.4
- ;, 9.2
- ;[…∣…∣…], 9.2
- <, 3.2.2
- <=, 3.2.2
- >, 3.2.2
- >=, 3.2.2
- ?, 8.2.2
- ?=, 3.2.2
- %, 12.2.2
- &, 3.1.4
- _, 1.2.11
- {A}+{B}, 3.1.4
- {x:A ∣ (P x)}, 3.1.4
- {x:A & (P x)}, 3.1.4
- A*B, 3.1.3
- A+{B}, 3.1.4
- A+B, 3.1.3
- Abbreviations, 12.3
- Abort, 7.1.5
- About, 6.1.1
- Absolute names, 2.6.2
- Acc, 3.1.6
- Acc_inv, 3.1.6
- Acc_rect, 3.1.6
- Add Field, 8.12.11, 23.8
- Add Legacy Abstract Ring, 23.9.2
- Add Legacy Abstract Semi Ring, 23.9.2
- Add Legacy Field, 23.9.4
- Add Legacy Ring, 23.9.1, 23.9.2
- Add Legacy Semi Ring, 23.9.2
- Add Legacy Semi Ring, 23.9.1
- Add LoadPath, 6.6.3
- Add ML Path, 6.6.7
- Add Morphism, 25.9
- Add Parametric Morphism, 25.2
- Add Parametric Relation, 25.2
- Add Printing If ident, 2.2.4
- Add Printing Let ident, 2.2.4
- Add Rec LoadPath, 6.6.4
- Add Rec ML Path, 6.6.8
- Add Relation, 25.2
- Add Ring, 8.12.10, 23.5
- Add Setoid, 25.9
- Admit Obligations, 22.2
- Admitted, 1.3.5, 7.1.3
- Arguments Scope, 12.2.2
- Arithmetical notations, 3.2.2
- Arity, 4.5.3
- Associativity, 12.1.2
- Axiom, 1.3.1
- Axiom (and coercions), 17.6.1
- abstract, 9.2
- abstractions, 1.2.7
- absurd, 3.1.2, 8.4.1
- absurd_set, 3.1.4
- admit, 8.3.17
- all, 3.1.2
- and, 3.1.2
- and_rect, 3.1.4
- app, 3.2.5
- appcontext
  - in pattern, 9.2
- applications, 1.2.9
- apply, 8.3.6
- apply … with, 8.3.6
- apply … in, 8.3.9
- assert, 8.3.8
- assert as, 8.3.8
- assert by, 8.3.8
- assumption, 8.3.1
- auto, 8.12.1
- autorewrite, 8.12.13
- autounfold, 8.12.3
- Back, 6.7.2
- BackTo, 6.7.3
- Backtrack, 6.7.3
- Bad Magic Number, 6.5.1
- Bind Scope, 12.2.2
- Binding list, 8.3.22
- BNF metasyntax, 1
- β-reduction, 4.3, 4.3
- binders, 1.2.6
- bool, 3.1.3
- bool_choice, 3.1.4
- byte-code, 13.1
- Calculus of (Co)Inductive Constructions, 4
- Calculus of (Co)Inductive Constructions, 4
- Canonical Structure, 2.7.15
- Cases, 16
- Cast, 1.2.10
- Cd, 6.6.2
- Check, 6.3.1
- Choice, 3.1.4
- Choice2, 3.1.4
- CIC, 4
- Class, 18.6.1
- Clauses, 8.5
- Close Scope, 12.2.1
- Coercion, 2.8, 17.6.1, 17.6.1
- Coercions, 2.8
  - and modules, 17.11
  - and records, 17.9
  - and sections, 17.10
  - classes, 17.2
  - Funclass, 17.3
  - identity, 17.4
  - inheritance graph, 17.5
  - presentation, 17
  - Sortclass, 17.3
- CoFixpoint, 1.3.4, 1.3.5
- CoFixpoint … where …, 12.1.8
- CoInductive, 1.3.3
- CoInductive (and coercions), 17.6.1
- Combined Scheme, 8.14.2, 10.3.1
- Comments, 1.1
- Compiled files, 6.5
- Compute, 6.3.3
- Conjecture, 1.3.1
- Connectives, 3.1.2
- Constant, 1.3.2
- Context, 4.2
- Context, 18.6.4
- Contributions, 3.3
- Conversion rules, 4.3
- Conversion tactics, 8.5
- coqdep, 14.2
- coqdoc, 14.4
- coq_Makefile, 14.3
- coqmktop, 14.1
- coq-tex, 14.6
- Corollary, 1.3.5
- CreateHintDb, 8.13.1
- case, 8.7.2
- case_eq, 8.7.2
- cbv, 8.5.1
- change, 8.3.12
- change … in, 8.3.12
- classical_left, 8.11.1
- classical_right, 8.11.1
- clear, 8.3.2
- clear dependent, 8.3.2
- clearbody, 8.3.2
- cofix, 8.3.14
- compare, 8.9.2
- compute, 8.5.1, 8.5.1
- congruence, 8.12.8
- conj, 3.1.2
- constr_eq, 8.3.18
- constructor, 8.6.1
- context
  - in expression, 9.2
  - in pattern, 9.2
- contradict, 8.4.3
- contradiction, 8.4.2
- coqc, 13
- coqide, 15
- coqtop, 13
- cut, 8.3.8
- cutrewrite, 8.8.2
- Datatypes, 3.1.3
- Debugger, 14.1
- Declarations, 1.3.1
- Declare Implicit Tactic, 8.13.6
- Declare Instance, 18.6.2
- Declare Left Step, 8.8.8
- Declare ML Module, 6.5.3
- Declare Right Step, 8.8.8
- Defined, 1.3.5, 7.1.2
- Definition, 1.3.2
- Definitions, 1.3.2
- Delimit Scope, 12.2.2
- Dependencies, 14.2
- Derive Dependent Inversion, 8.10.2
- Derive Dependent Inversion_clear, 8.10.2
- Derive Inversion, 8.10.2
- Derive Inversion_clear, 8.10.2
- Derive Inversion_clear … with, 8.10.2
- Disjunctive/conjunctive introduction patterns, 8.7.3
- DPL, 11
- Drop, 6.8.2
- decide equality, 8.9.1
- decompose, 8.7.6
- decompose record, 8.7.6
- decompose sum, 8.7.6
- δ-reduction, 1.3.2, 4.3, 4.3
- dependent destruction, 8.7.5
- dependent induction, 8.7.5
- dependent induction … generalizing, 8.7.5
- dependent inversion, 8.10.1
- dependent inversion … as , 8.10.1
- dependent inversion … as … with, 8.10.1
- dependent inversion … with, 8.10.1
- dependent inversion_clear, 8.10.1
- dependent inversion_clear … as, 8.10.1
- dependent inversion_clear … as … with, 8.10.1
- dependent inversion_clear … with, 8.10.1
- dependent rewrite ->, 8.9.6
- dependent rewrite <-, 8.9.6
- destruct, 8.7.2
- discriminate, 8.9.3
- discrR, 3.2.4
- do, 9.2
- Elimination
  - Empty elimination, 4.5.4
  - Singleton elimination, 4.5.4
- Elimination sorts, 4.5.4
- Emacs, 14.7
- End, 2.4.2, 2.5.2, 2.5.5
- Environment, 1.3.1, 1.3.2, 4.2
- Environment variables, 13.4
- Equality, 3.1.2
- Eval, 6.3.2
- Example, 1.3.2
- Exc, 3.1.4
- Existential, 7.1.8
- Existing Class, 18.6.1
- Existing Instance, 18.6.3
- Explicitly given implicit arguments, 2.7.11
- Export, 2.5.8
- Extract Constant, 21.2.4
- Extract Inductive, 21.2.4
- Extraction, 21
- Extraction, 6.3.4, 21.1
- Extraction Blacklist, 21.2.5
- Extraction Implicit, 21.2.3
- Extraction Inline, 21.2.2
- Extraction Language, 21.2.1
- Extraction Module, 21.1
- Extraction NoInline, 21.2.2
- eapply, 8.3.6, 10.2
- eapply … in, 8.3.9
- eassumption, 8.3.1
- eauto, 8.12.2
- ecase, 8.7.2
- econstructor, 8.6.1
- edestruct, 8.7.2
- ediscriminate, 8.9.3
- eelim, 8.7.1
- eexact, 8.2.1
- eexists, 8.6.1
- einduction, 8.7.1
- einjection, 8.9.4
- eleft, 8.6.1
- elim … using, 8.7.1
- elimtype, 8.7.1
- eq, 3.1.2
- eq_add_S, 3.1.5
- eq_ind_r, 3.1.2
- eq_rec_r, 3.1.2
- eq_rect, 3.1.2, 3.1.4
- eq_rect_r, 3.1.2
- eq_S, 3.1.5
- erewrite, 8.8.1
- eright, 8.6.1
- error, 3.1.4
- esimplify_eq, 8.9.5
- esplit, 8.6.1
- η-conversion, 4.3
- η-reduction, 4.3
- eval
  - in Ltac, 9.2
- evar, 8.3.15
- ex, 3.1.2
- ex2, 3.1.2
- ex_intro, 3.1.2
- ex_intro2, 3.1.2
- exact, 8.2.1
- exfalso, 8.4.4
- exist, 3.1.4
- exist2, 3.1.4
- exists, 3.1.2, 8.6.1
- exists2, 3.1.2
- existT, 3.1.4
- existT2, 3.1.4
- Fact, 1.3.5
- False, 3.1.2
- False_rec, 3.1.4
- False_rect, 3.1.4
- Fix, 4.5.5
- Fix_F, 3.1.6
- Fix_F_eq, 3.1.6
- Fix_F_inv, 3.1.6
- Fixpoint, 1.3.4, 1.3.5
- Fixpoint … where …, 12.1.8
- Focus, 7.2.5
- Function, 2.3
- Functional Scheme, 8.15, 10.4
- f_equal, 3.1.2, 8.8.9
- f_equali, 3.1.2
- fail, 9.2
- false, 3.1.3
- field, 8.12.11, 23.7
- field_simplify, 8.12.11, 23.7
- field_simplify_eq, 8.12.11, 23.7
- first, 9.2
- firstorder, 8.12.7
- firstorder tactic, 8.12.7
- firstorder using, 8.12.7
- firstorder with, 8.12.7
- fix, 8.3.13
- fix identi{…}, 1.2.14
- fix_eq, 3.1.6
- flat_map, 3.2.5
- fold, 8.5.6
- fold_left, 3.2.5
- fold_right, 3.2.5
- form, 1.2.5
- fourier, 8.12.12
- fresh
  - in Ltac, 9.2
- fst, 3.1.3
- fun
  - in Ltac, 9.2
- functional induction, 8.7.7, 10.4
- Gallina, 1, 2
- gallina, 14.8
- Generalizable Variables, 2.7.17
- Global, 6.11.1
- Global Implicit Arguments, 2.7.4, 2.7.5
- Global Set, 6.2.1
- Global Unset, 6.2.2
- Goal, 7.1.1
- Goal clauses, 8.5
- Guarded, 7.3.2
- ge, 3.1.5
- generalize, 8.3.10
- generalize dependent, 8.3.10
- goal, 8
- gt, 3.1.5
- Head normal form, 4.3
- Hint, 8.13.1
- Hint Constructors, 8.13.1
- Hint Extern, 8.13.1
- Hint Immediate, 8.13.1
- Hint Opaque, 8.13.1
- Hint Resolve, 8.13.1
- Hint Rewrite, 8.13.4
- Hint Transparent, 8.13.1
- Hint Unfold, 8.13.1
- Hints databases, 8.13.1
- Hypotheses, 1.3.1
- Hypothesis, 1.3.1
- Hypothesis (and coercions), 17.6.1
- has_evar, 8.3.20
- head, 3.2.5
- hnf, 8.5.3
- I, 3.1.2
- Identity Coercion, 17.6.2
- IF_then_else, 3.1.2
- Implicit Arguments, 2.7.4, 2.7.5
- Implicit arguments, 2.7
- Implicit Types, 2.7.16
- Import, 2.5.8
- Include, 2.5.1, 2.5.4
- Inductive, 1.3.3, 1.3.3
- Inductive (and coercions), 17.6.1
- Inductive … where …, 12.1.8
- Inductive definitions, 1.3.3
- Infix, 12.1.6
- Inline, 2.5.4
- Inspect, 6.1.2
- Instance, 18.6.2
- Interpretation scopes, 12.2
- Introduction patterns, 8.7.3
- IsSucc, 3.1.5
- ident, 1.1
- identity, 3.1.3
- idtac, 9.2
- if ... then ... else, 2.2.2
- iff, 3.1.2
- induction, 8.7.1
- info, 9.2
- injection, 8.9.4
- injection … as, 8.9.4
- inl, 3.1.3
- inleft, 3.1.4
- inr, 3.1.3
- inright, 3.1.4
- instantiate, 8.3.16
- integer, 1.1
- intro, 8.3.5
- intro after, 8.3.5
- intro at bottom, 8.3.5
- intro at top, 8.3.5
- intro before, 8.3.5
- intros, 8.3.5
- intros intro_pattern, 8.7.3
- intros until, 8.3.5, 8.3.5
- intuition, 8.12.5
- inversion, 8.10.1, 10.5
- inversion … as, 8.10.1
- inversion … as … in, 8.10.1
- inversion … in, 8.10.1
- inversion … using, 8.10.1
- inversion … using … in, 8.10.1
- inversion_clear, 8.10.1
- inversion_clear … as … in, 8.10.1
- inversion_clear … in, 8.10.1
- inversion_cleardots as, 8.10.1
- ι-reduction, 4.3, 4.3, 4.5.4, 4.5.5
- is_evar, 8.3.19
- is_var, 8.3.21
- LATEX, 14.6
- Lemma, 1.3.5
- Let, 1.3.2
- Lexical conventions, 1.1
- Libraries, 2.6.1
- Load, 6.4.1
- Load Verbose, 6.4.1
- Loadpath, 6.6
- Local, 6.11.1
- Local Coercion, 17.6.1, 17.6.1
- Local definitions, 1.2.12
- Local Implicit Arguments, 2.7.4, 2.7.5
- Local Set, 6.2.1
- Local Strategy, 6.10.3
- Local Unset, 6.2.2
- Locate, 6.3.10, 12.1.10
- Locate File, 6.6.10
- Locate Library, 6.6.11
- Locate Module, 2.5.11
- Logical paths, 2.6.1
- Ltac
  - eval, 9.2
  - external, 9.2
  - fresh, 9.2
  - fun, 9.2
  - lazymatch, 9.2
  - lazymatch goal, 9.2
  - lazymatch reverse goal, 9.2
  - let, 9.2
  - let rec, 9.2
  - match, 9.2
  - match goal, 9.2
  - match reverse goal, 9.2
  - type of, 9.2

- Ltac, 9.3
- λ-calculus, 4.1.3
- lapply, 8.3.6
- lazy, 8.5.1
- lazymatch
  - in Ltac, 9.2
- lazymatch goal
  - in Ltac, 9.2
- lazymatch reverse goal
  - in Ltac, 9.2
- le, 3.1.5
- le_n, 3.1.5
- le_S, 3.1.5
- left, 3.1.4, 8.6.1
- legacy field, 23.9.3
- legacy ring, 23.9.1
- length, 3.2.5
- let
  - in Ltac, 9.2
- let ’... in, 2.2.3
- let ... in, 2.2.3
- let rec
  - in Ltac, 9.2
- let-in, 1.2.12
- lia, 20.3
- local context, 7
- lt, 3.1.5
- Makefile, 14.3
- Man pages, 14.9
- ML-like patterns, 2.2.1, 16
- Module, 2.5.1, 2.5.3
- Module Type, 2.5.4
- Modules, 2.5
- map, 3.2.5
- match
  - in Ltac, 9.2
- match…with…end, 1.2.13, 2.2, 4.5.4
- match goal
  - in Ltac, 9.2
- match reverse goal
  - in Ltac, 9.2
- mod, 3.2.2
- move, 8.3.3
- mult, 3.1.5
- mult_n_O, 3.1.5
- mult_n_Sm, 3.1.5
- Naming introduction patterns, 8.7.3
- Next Obligation, 22.2
- None, 3.1.3
- Normal form, 4.3
- Notation, 12.1, 12.3
- Notations for lists, 3.2.5
- Notations for real numbers, 3.2.4
- n_Sn, 3.1.5
- nat, 3.1.3
- nat_case, 3.1.5
- nat_double_ind, 3.1.5
- nat_scope, 3.2.3
- native code, 13.1
- not, 3.1.2
- not_eq_S, 3.1.5
- notT, 3.1.7
- nsatz, 24.1
- nth, 3.2.5
- num, 1.1
- O, 3.1.3
- O_S, 3.1.5
- Obligation, 22.2
- Obligation Tactic, 22.2
- Obligations, 22.2
- Occurrences clauses, 8.3.23
- Opaque, 6.10.1
- Open Scope, 12.2.1
- Options of the command line, 13.5
- omega, 8.12.9, 19.1
- option, 3.1.3
- or, 3.1.2
- or_introl, 3.1.2
- or_intror, 3.1.2
- Parameter, 1.3.1
- Parameter (and coercions), 17.6.1
- Parameters, 1.3.1
- Peano’s arithmetic, 3.2.3
- Physical paths, 2.6.1
- Positivity, 4.5.3
- Precedences, 12.1.2
- Predicative Calculus of (Co)Inductive Constructions, 4
- Preterm, 22.2
- Print, 6.1.1
- Print All, 6.1.2
- Print Assumptions, 6.3.5
- Print Canonical Projections, 2.7.15
- Print Classes, 17.7.1
- Print Coercion Paths, 17.7.4
- Print Coercions, 17.7.2
- Print Extraction Inline, 21.2.2
- Print Grammar constr, 12.1.4
- Print Grammar pattern, 12.1.4
- Print Graph, 17.7.3
- Print Hint, 8.13.3
- Print HintDb, 8.13.3
- Print Implicit, 2.7.12
- Print Libraries, 6.5.2
- Print LoadPath, 6.6.6
- Print Ltac, 9.3.2
- Print ML Modules, 6.5.4
- Print ML Path, 6.6.9
- Print Module, 2.5.9
- Print Module Type, 2.5.10
- Print Opaque Dependencies, 6.3.5
- Print Scope, 12.2.5
- Print Scopes, 12.2.5
- Print Section, 6.1.2
- Print Table Printing If, 2.2.4
- Print Table Printing Let, 2.2.4
- Print Term, 6.1.1
- Print Universes, 2.10
- Print Visibility, 12.2.5
- Print XML, 14.5.5
- Program, 22
- Program Definition, 22.1.1
- Program Fixpoint, 22.1.2
- Program Instance, 18.1, 18.6.2
- Program Lemma, 22.1.3
- Programming, 3.1.3
- Prompt, 7
- Proof, 1.3.5, 7.1.4
- Proof editing, 7
- Proof General, 14.7.2
- Proof rendering, 14.5
- Proof term, 7
- Proof with, 8.13.6
- Prop, 1.2.5, 4.1.1
- Proposition, 1.3.5
- Pwd, 6.6.1
- pair, 3.1.3
- pairT, 3.1.7
- pattern, 8.5.7
- pCIC, 4
- plus, 3.1.5
- plus_n_O, 3.1.5
- plus_n_Sm, 3.1.5
- pose, 8.3.7
- pose proof, 8.3.8, 8.3.8
- pred, 3.1.5
- pred_Sn, 3.1.5
- prod, 3.1.3
- prodT, 3.1.7
- products, 1.2.8
- progress, 9.2
- proj1, 3.1.2
- proj2, 3.1.2
- projT1, 3.1.4
- projT2, 3.1.4
- psatz, 20.1
- Qed, 1.3.5, 7.1.2
- Qualified identifiers, 2.6.2
- Quantifiers, 3.1.2
- Quit, 6.8.1
- qualid, 2.7.11
- quote, 8.10.4, 10.8
- Record, 2.1
- Recursion, 3.1.6
- Recursive arguments, 4.5.5
- Recursive Extraction, 21.1
- Recursive Extraction Module, 21.1
- Remark, 1.3.5
- Remove LoadPath, 6.6.5
- Remove Printing If ident, 2.2.4
- Remove Printing Let ident, 2.2.4
- Require, 6.5.1, 6.5.1
- Require Export, 6.5.1
- ReservedNotation, 12.1.7
- Reset, 6.7.1
- Reset Extraction Inline, 21.2.2
- Reset Initial, 6.7.4
- Resource file, 13.3
- Restart, 7.2.4
- Restore State, 6.7.4
- Resume, 7.1.7
- red, 8.5.2
- refine, 8.2.2, 10.1
- refl_equal, 3.1.2
- refl_identity, 3.1.3
- reflexivity, 8.8.4
- remember, 8.3.7
- rename, 8.3.4
- repeat, 9.2
- replace … with, 8.8.3
- rev, 3.2.5
- revert, 8.3.11
- revert dependent, 8.3.11
- rewrite, 8.8.1
- rewrite ->, 8.8.1
- rewrite <-, 8.8.1
- rewrite … at, 8.8.1
- rewrite … by, 8.8.1
- rewrite … in, 8.8.1
- right, 3.1.4, 8.6.1
- ring, 8.12.10, 23, 23.4
- ring_simplify, 8.12.10, 23.4
- rtauto, 8.12.6
- S, 3.1.3
- Save, 7.1.2
- Scheme, 8.14, 10.3
- Scheme Equality, 8.14
- Schemes, 8.14
- Script file, 6.4
- Search, 6.3.6
- SearchAbout, 6.3.7
- SearchPattern, 6.3.8
- SearchRewrite, 6.3.9
- Section, 2.4.1
- Sections, 2.4
- Set, 6.2.1
- Set, 1.2.5, 4.1.1
- Set Automatic Coercions Import, 17.11
- Set Automatic Introduction, 7.4.3
- Set Contextual Implicit, 2.7.8
- Set Default Timeout, 6.8.5
- Set Elimination Schemes, 8.14.1
- Set Equality Schemes, 8.14.1
- Set Extraction AutoInline, 21.2.2
- Set Extraction Optimize, 21.2.2
- Set Firstorder Depth, 8.12.7
- Set Hyps Limit, 7.4.1
- Set Implicit Arguments, 2.7.6
- Set Ltac Debug, 9.4
- Set Maximal Implicit Insertion, 2.7.10
- Set Printing All, 2.9
- Set Printing Coercion, 17.8.2
- Set Printing Coercions, 17.8.1
- Set Printing Depth, 6.9.6
- Set Printing Implicit, 2.7.13
- Set Printing Implicit Defensive, 2.7.13
- Set Printing Matching, 2.2.4
- Set Printing Notations, 12.1.9
- Set Printing Synth, 2.2.4
- Set Printing Universes, 2.10
- Set Printing Width, 6.9.3
- Set Printing Wildcard, 2.2.4
- Set Reversible Pattern Implicit, 2.7.9
- Set Silent, 6.9.1
- Set Strict Implicit, 2.7.7
- Set Strongly Strict Implicit, 2.7.7
- Set Transparent Obligations, 22.2
- Set Undo, 7.2.2
- Set Virtual Machine, 6.10.5
- Set Whelp Getter, 6.3.11
- Set Whelp Server, 6.3.11
- Show, 7.3.1
- Show Conjectures, 7.3.1
- Show Existentials, 7.3.1
- Show Implicits, 7.3.1
- Show Intro, 7.3.1
- Show Intros, 7.3.1
- Show Obligation Tactic, 22.2
- Show Proof, 7.3.1
- Show Script, 7.3.1
- Show Tree, 7.3.1
- Show XML Proof, 14.5.5
- Silent mode, 6.9.1
- Solve Obligations, 22.2
- Some, 3.1.3
- Sort-polymorphism of inductive families, 4.5.3
- Sorts, 1.2.5, 1.2.5, 4.1.1
- Strategy, 6.10.3
- Structure, 17.9
- SubClass, 17.6.2
- Substitution, 4.1.3
- Suspend, 7.1.6
- set, 8.3.7
- setoid_reflexivity, 25.7
- setoid_replace, 25, 25.7
- setoid_rewrite, 25.7
- setoid_symmetry, 25.7
- setoid_transitivity, 25.7
- sig, 3.1.4
- sig2, 3.1.4
- sigT, 3.1.4
- sigT2, 3.1.4
- simpl, 8.5.4
- simpl … in, 8.5.4
- simple apply, 8.3.6
- simple apply … in, 8.3.9
- simple destruct, 8.7.2
- simple eapply … in, 8.3.9
- simple induction, 8.7.1
- simple inversion, 8.10.1
- simple inversion … as, 8.10.1
- simplify_eq, 8.9.5
- snd, 3.1.3
- solve, 9.2
- sort, 1.2.1
- specialize, 8.3.8
- specif, 1.2.5
- split, 8.6.1
- split_Rabs, 3.2.4
- split_Rmult, 3.2.4
- stepl, 8.8.8
- stepr, 8.8.8
- string, 1.1
- subgoal, 8
- subst, 8.8.7
- sum, 3.1.3
- sumbool, 3.1.4
- sumor, 3.1.4
- sym_eq, 3.1.2
- sym_not_eq, 3.1.2
- symmetry, 8.8.5
- symmetry in, 8.8.5
- Tactic Definition, 8.16
- Tactic macros, 8.16
- Tacticals, 9.2
  - tactic1;tactic2, 9.2
  - tactic0;[tactic1∣…∣tacticn], 9.2
  - abstract, 9.2
  - do, 9.2
  - fail, 9.2
  - first, 9.2
  - idtac, 9.2
  - info, 9.2
  - ∣∣, 9.2
  - repeat, 9.2
  - solve, 9.2
  - try, 9.2
- Tactics, 8
- Terms, 1.2
- Test, 6.2.3
- Test Default Timeout, 6.8.7
- Test Ltac Debug, 9.4
- Test Printing Depth, 6.9.8
- Test Printing If for ident, 2.2.4
- Test Printing Let for ident, 2.2.4
- Test Printing Matching, 2.2.4
- Test Printing Synth, 2.2.4
- Test Printing Width, 6.9.5
- Test Printing Wildcard, 2.2.4
- Test Virtual Machine, 6.10.7
- Test Whelp Getter, 6.3.11
- Test Whelp Server, 6.3.11
- Theorem, 1.3.5, 7.1
- Theories, 3
- Time, 6.8.3
- Timeout, 6.8.4
- Transparent, 6.10.2
- True, 3.1.2
- Type, 1.2.5, 4.1.1
- Type of constructor, 4.5.3
- Typeclasses eauto, 18.6.6
- Typeclasses Opaque, 18.6.5
- Typeclasses Transparent, 18.6.5
- Typing rules, 4.2, 8.3
  - App, 4.2, 8.3.8
  - Ax, 4.2
  - Const, 4.2
  - Conv, 4.3, 8.3.5, 8.3.12
  - Fix, 4.5.5
  - Lam, 4.2, 8.3.5
  - Let, 4.2, 8.3.5
  - match, 4.5.4
  - Prod, 4.2
  - Prod (impredicative Set), 4.7
  - Var, 4.2, 8.3.1
- tactic, 8.1
- tail, 3.2.5
- tauto, 8.12.4
- term, 1.2.1
- trans_eq, 3.1.2
- transitivity, 8.8.6
- trivial, 8.12.1
- true, 3.1.3
- try, 9.2
- tt, 3.1.3
- type, 1.2.2, 1.2.5
- type of
  - in Ltac, 9.2
- type_scope, 12.2.3
- Undo, 7.2.1
- Unfocus, 7.2.6
- Unset, 6.2.2
- Unset Automatic Coercions Import, 17.11
- Unset Automatic Introduction, 7.4.3
- Unset Contextual Implicit, 2.7.8
- Unset Default Timeout, 6.8.6
- Unset Extraction AutoInline, 21.2.2
- Unset Extraction Optimize, 21.2.2
- Unset Hyps Limit, 7.4.2
- Unset Implicit Arguments, 2.7.6
- Unset Ltac Debug, 9.4
- Unset Maximal Implicit Insertion, 2.7.10
- Unset Printing All, 2.9
- Unset Printing Coercion, 17.8.2
- Unset Printing Coercions, 17.8.1
- Unset Printing Depth, 6.9.7
- Unset Printing Implicit, 2.7.13
- Unset Printing Implicit Defensive, 2.7.13
- Unset Printing Matching, 2.2.4
- Unset Printing Notations, 12.1.9
- Unset Printing Synth, 2.2.4
- Unset Printing Universes, 2.10
- Unset Printing Width, 6.9.4
- Unset Printing Wildcard, 2.2.4
- Unset Reversible Pattern Implicit, 2.7.9
- Unset Silent, 6.9.2
- Unset Strict Implicit, 2.7.7
- Unset Strongly Strict Implicit, 2.7.7
- Unset Undo, 7.2.3
- Unset Virtual Machine, 6.10.6
- unfold, 8.5.5
- unfold … in, 8.5.5
- unit, 3.1.3
- Variable, 1.3.1
- Variable (and coercions), 17.6.1
- Variables, 1.3.1
- value, 3.1.4
- vm_compute, 8.5.1, 8.5.1
- Well founded induction, 3.1.6
- Well foundedness, 3.1.6
- Whelp Elim, 6.3.11
- Whelp Hint, 6.3.11
- Whelp Instance, 6.3.11
- Whelp Locate, 6.3.11
- Whelp Match, 6.3.11
- Write State, 6.7.5
- well_founded, 3.1.6
- XML exportation, 14.5
- ζ-reduction, 4.3, 4.3