# Coq Reference Manual

# Global Index

- ∣∣, 9.2
- *, 3.1.3, 3.2.2
- * (command), 7.2.7
- +, 3.1.3, 3.2.2
- + (command), 7.2.7
- -, 3.2.2
- - (command), 7.2.7
- /, 3.2.2
- 2-level approach, 8.15.2
- ;, 9.2
- ;[…∣…∣…], 9.2
- <, 3.2.2
- <=, 3.2.2
- >, 3.2.2
- >=, 3.2.2
- ?, 8.2.3
- ?=, 3.2.2
- %, 12.2.2
- &, 3.1.4
- _, 1.2.11
- {, 7.2.6
- {A}+{B}, 3.1.4
- {x:A ∣ (P x)}, 3.1.4
- {x:A & (P x)}, 3.1.4
- }, 7.2.6
- @, 2.7.11
- A*B, 3.1.3
- A+{B}, 3.1.4
- A+B, 3.1.3
- Abbreviations, 12.3
- Abort, 7.1.6
- 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.17.3, 24.8
- Add Legacy Abstract Ring, 24.9.2
- Add Legacy Abstract Semi Ring, 24.9.2
- Add Legacy Field, 24.9.4
- Add Legacy Ring, 24.9.1, 24.9.2
- Add Legacy Semi Ring, 24.9.2
- Add Legacy Semi Ring, 24.9.1
- Add LoadPath, 6.6.3
- Add ML Path, 6.6.7
- Add Morphism, 26.9
- Add Parametric Morphism, 26.2
- Add Parametric Relation, 26.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, 26.2
- Add Ring, 8.17.2, 24.5
- Add Setoid, 26.9
- Admit Obligations, 23.2
- Admitted, 1.3.5, 7.1.3
- Arguments, 2.7.4, 2.7.5, 2.7.5, 2.7.12, 8.7.4, 12.2.2
- Arithmetical notations, 3.2.2
- Arity, 4.5.3
- Associativity, 12.1.2
- Axiom, 1.3.1
- Axiom (and coercions), 18.6.1
- abstract, 9.2
- abstractions, 1.2.7
- absurd, 3.1.2, 8.4.6
- absurd_set, 3.1.4
- admit, 8.4.5
- 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.2.4
- apply … in, 8.2.5
- apply … with, 8.2.4
- assert, 8.4.1
- assert as, 8.4.1
- assert by, 8.4.1
- assumption, 8.2.2
- auto, 8.8.1
- autorewrite, 8.8.4
- autounfold, 8.8.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.1.1
- BNF metasyntax, 1
- Bullets, 7.2.7
- β-reduction, 4.3, 4.3
- binders, 1.2.6
- bool, 3.1.3
- bool_choice, 3.1.4
- byte-code, 14.1
- Calculus of (Co)Inductive Constructions, 4
- Calculus of (Co)Inductive Constructions, 4
- Canonical Structure, 2.7.18
- Cases, 17
- Cast, 1.2.10
- Cd, 6.6.2
- Check, 6.3.1
- Choice, 3.1.4
- Choice2, 3.1.4
- CIC, 4
- Class, 19.6.1
- Clauses, 8.7
- Close Scope, 12.2.1
- Coercion, 2.8, 18.6.1, 18.6.1
- Coercions, 2.8
  - and modules, 18.11
  - and records, 18.9
  - and sections, 18.10
  - classes, 18.2
  - Funclass, 18.3
  - identity, 18.4
  - inheritance graph, 18.5
  - presentation, 18
  - Sortclass, 18.3
- CoFixpoint, 1.3.4, 1.3.5
- CoFixpoint … where …, 12.1.8
- CoInductive, 1.3.3, 2.1
- CoInductive (and coercions), 18.6.1
- Combined Scheme, 13.1.2
- 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, 19.6.4
- Contributions, 3.3
- Conversion rules, 4.3
- Conversion tactics, 8.7
- coqdep, 15.2
- coqdoc, 15.4
- coq_Makefile, 15.3
- coqmktop, 15.1
- coq-tex, 15.6
- Corollary, 1.3.5
- CreateHintDb, 8.9.1
- case, 8.5.1
- case_eq, 8.5.1
- cbv, 8.7.1
- change, 8.6.9
- change … in, 8.6.9
- classical_left, 8.16.1
- classical_right, 8.16.1
- clear, 8.3.3
- clear dependent, 8.3.3
- clearbody, 8.3.3
- cofix, 8.5.10
- compare, 8.14.2
- compute, 8.7.1, 8.7.1
- congruence, 8.10.5
- conj, 3.1.2
- constr_eq, 8.12.1
- constructor, 8.2.6
- context
  - in expression, 9.2
  - in pattern, 9.2
- contradict, 8.4.8
- contradiction, 8.4.7
- coqc, 14
- coqide, 16
- coqtop, 14
- cut, 8.4.1
- cutrewrite, 8.6.2
- Datatypes, 3.1.3
- Debugger, 15.1
- Declarations, 1.3.1
- Declare Implicit Tactic, 8.9.6
- Declare Instance, 19.6.2
- Declare Left Step, 8.6.8
- Declare ML Module, 6.5.3
- Declare Right Step, 8.6.8
- Defined, 1.3.5, 7.1.2
- Definition, 1.3.2
- Definitions, 1.3.2
- Delimit Scope, 12.2.2
- Dependencies, 15.2
- Derive Dependent Inversion, 13.3
- Derive Dependent Inversion_clear, 13.3
- Derive Inversion, 13.3
- Derive Inversion_clear, 13.3
- Disjunctive/conjunctive introduction patterns, 8.3.2
- DPL, 11
- Drop, 6.9.2
- decide equality, 8.14.1
- decompose, 8.3.8
- decompose record, 8.3.8
- decompose sum, 8.3.8
- δ-reduction, 1.3.2, 4.3, 4.3
- dependent destruction, 8.5.4
- dependent induction, 8.5.4
- dependent induction … generalizing, 8.5.4
- dependent inversion, 8.5.8
- dependent inversion … as , 8.5.8
- dependent inversion … as … with, 8.5.8
- dependent inversion … with, 8.5.8
- dependent inversion_clear, 8.5.8
- dependent inversion_clear … as, 8.5.8
- dependent inversion_clear … as … with, 8.5.8
- dependent inversion_clear … with, 8.5.8
- dependent rewrite ->, 8.14.4
- dependent rewrite <-, 8.14.4
- destruct, 8.5.1
- discriminate, 8.5.6
- discrR, 3.2.4
- do, 9.2
- double induction, 8.5.3
- Elimination
  - Empty elimination, 4.5.4
  - Singleton elimination, 4.5.4
- Elimination sorts, 4.5.4
- Emacs, 15.7
- End, 2.4.2, 2.5.2, 2.5.5
- Environment, 1.3.1, 1.3.2, 4.2
- Environment variables, 14.4
- Equality, 3.1.2
- Eval, 6.3.2
- Example, 1.3.2
- Exc, 3.1.4
- Existential, 7.1.7
- Existing Class, 19.6.1
- Existing Instance, 19.6.3
- Existing Instances, 19.6.3
- Explicitly given implicit arguments, 2.7.11
- Export, 2.5.8
- Extract Constant, 22.2.4
- Extract Inductive, 22.2.4
- Extraction, 22
- Extraction, 6.3.4, 22.1
- Extraction Blacklist, 22.2.5
- Extraction Implicit, 22.2.3
- Extraction Inline, 22.2.2
- Extraction Language, 22.2.1
- Extraction Library, 22.1
- Extraction NoInline, 22.2.2
- eapply, 8.2.4
- eapply … in, 8.2.5
- eassumption, 8.2.2
- eauto, 8.8.2
- ecase, 8.5.1
- econstructor, 8.2.6
- edestruct, 8.5.1
- ediscriminate, 8.5.6
- eelim, 8.5.2
- eexact, 8.2.1
- eexists, 8.2.6
- einduction, 8.5.2
- einjection, 8.5.7
- eleft, 8.2.6
- elim … using, 8.5.2
- elimtype, 8.5.2
- 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_refl, 3.1.2
- eq_S, 3.1.5
- eq_sym, 3.1.2
- eq_trans, 3.1.2
- erewrite, 8.6.1
- eright, 8.2.6
- error, 3.1.4
- esimplify_eq, 8.14.3
- esplit, 8.2.6
- η-conversion, 4.3
- eval
  - in Ltac, 9.2
- evar, 8.4.3
- 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.9
- exist, 3.1.4
- exist2, 3.1.4
- exists, 3.1.2, 8.2.6
- 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.3
- Function, 2.3
- Functional Scheme, 13.2
- f_equal, 3.1.2, 8.13.1
- f_equal i, 3.1.2
- fail, 9.2
- false, 3.1.3
- field, 8.17.3, 24.7
- field_simplify, 8.17.3, 24.7
- field_simplify_eq, 8.17.3, 24.7
- first, 9.2
- firstorder, 8.10.4
- firstorder tactic, 8.10.4
- firstorder using, 8.10.4
- firstorder with, 8.10.4
- fix, 8.5.9
- fix identi{…}, 1.2.14
- fix_eq, 3.1.6
- flat_map, 3.2.5
- fold, 8.7.6
- fold_left, 3.2.5
- fold_right, 3.2.5
- form, 1.2.5
- fourier, 8.17.4
- fresh
  - in Ltac, 9.2
- fst, 3.1.3
- fun
  - in Ltac, 9.2
- functional induction, 8.5.5, 13.2
- Gallina, 1, 2
- gallina, 15.8
- Generalizable Variables, 2.7.20
- Global, 6.12.1
- Global Arguments, 2.7.4, 2.7.5
- Global Set, 6.2.1
- Global Unset, 6.2.2
- Goal, 7.1.1
- Goal clauses, 8.7
- Grab Existential Variables, 7.1.8
- Guarded, 7.3.2
- ge, 3.1.5
- generalize, 8.4.2
- generalize dependent, 8.4.2
- goal, 8
- gt, 3.1.5
- Head normal form, 4.3
- Hint, 8.9.1
- Hint Constructors, 8.9.1
- Hint Extern, 8.9.1
- Hint Immediate, 8.9.1
- Hint Opaque, 8.9.1
- Hint Resolve, 8.9.1
- Hint Rewrite, 8.9.4
- Hint Transparent, 8.9.1
- Hint Unfold, 8.9.1
- Hints databases, 8.9.1
- Hypotheses, 1.3.1
- Hypothesis, 1.3.1
- Hypothesis (and coercions), 18.6.1
- has_evar, 8.12.4
- head, 3.2.5
- hnf, 8.7.3
- I, 3.1.2
- Identity Coercion, 18.6.2
- IF_then_else, 3.1.2
- Implicit Arguments, 2.7.13
- Implicit arguments, 2.7
- Implicit Types, 2.7.19
- Import, 2.5.8
- Include, 2.5.1, 2.5.4
- Inductive, 1.3.3, 1.3.3, 2.1
- Inductive (and coercions), 18.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, 19.6.2
- Interpretation scopes, 12.2
- Introduction patterns, 8.3.2
- 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.5.2
- info, 9.2
- injection, 8.5.7
- injection … as, 8.5.7
- inl, 3.1.3
- inleft, 3.1.4
- inr, 3.1.3
- inright, 3.1.4
- instantiate, 8.4.4
- integer, 1.1
- intro, 8.3.1
- intro after, 8.3.1
- intro at bottom, 8.3.1
- intro at top, 8.3.1
- intro before, 8.3.1
- intros, 8.3.1
- intros intro_pattern, 8.3.2
- intros until, 8.3.1, 8.3.1
- intuition, 8.10.2
- inversion, 8.5.8
- inversion … as, 8.5.8
- inversion … as … in, 8.5.8
- inversion … in, 8.5.8
- inversion … using, 8.5.8, 13.3
- inversion … using … in, 8.5.8
- inversion_clear, 8.5.8
- inversion_clear … as, 8.5.8
- inversion_clear … as … in, 8.5.8
- inversion_clear … in, 8.5.8
- ι-reduction, 4.3, 4.3, 4.5.4, 4.5.5
- is_evar, 8.12.3
- is_var, 8.12.5
- LATEX, 15.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.12.1
- Local Arguments, 2.7.4, 2.7.5
- Local Coercion, 18.6.1, 18.6.1
- Local definitions, 1.2.12
- Local Set, 6.2.1
- Local Strategy, 6.11.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.2.4
- lazy, 8.7.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.2.6
- legacy field, 24.9.3
- legacy ring, 24.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, 21.5
- local context, 7
- lra, 21.1
- lt, 3.1.5
- Makefile, 15.3
- Man pages, 15.9
- ML-like patterns, 2.2.1, 17
- 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.5
- mult, 3.1.5
- mult_n_O, 3.1.5
- mult_n_Sm, 3.1.5
- Naming introduction patterns, 8.3.2
- Next Obligation, 23.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, 14.1
- nia, 21.6
- not, 3.1.2
- not_eq_S, 3.1.5
- notT, 3.1.7
- nsatz, 25.1
- nth, 3.2.5
- num, 1.1
- O, 3.1.3
- O_S, 3.1.5
- Obligation, 23.2
- Obligation Tactic, 23.2
- Obligations, 23.2
- Occurrences clauses, 8.1.2
- Opaque, 6.11.1
- Open Scope, 12.2.1
- Options of the command line, 14.4.1
- omega, 8.17.1, 20.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), 18.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, 23.2
- Print, 6.1.1
- Print All, 6.1.2
- Print Assumptions, 6.3.5
- Print Canonical Projections, 2.7.18
- Print Classes, 18.7.1
- Print Coercion Paths, 18.7.4
- Print Coercions, 18.7.2
- Print Extraction Inline, 22.2.2
- Print Grammar constr, 12.1.4
- Print Grammar pattern, 12.1.4
- Print Graph, 18.7.3
- Print Hint, 8.9.3
- Print HintDb, 8.9.3
- Print Implicit, 2.7.14
- 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 Sorted Universes, 2.10
- 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, 15.5.5
- Program, 23
- Program Definition, 23.1.2
- Program Fixpoint, 23.1.3
- Program Instance, 19.1, 19.6.2
- Program Lemma, 23.1.4
- Programming, 3.1.3
- Prompt, 7
- Proof, 1.3.5, 7.1.4
- Proof editing, 7
- Proof General, 15.7.2
- Proof rendering, 15.5
- Proof term, 7
- Proof using, 7.1.5
- Proof with, 8.9.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.7.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.4.1, 8.4.1
- 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, 21.1
- Qed, 1.3.5, 7.1.2
- Qualified identifiers, 2.6.2
- Quantifiers, 3.1.2
- Quit, 6.9.1
- qualid, 2.7.11
- quote, 8.15.2, 10.3
- Record, 2.1
- Recursion, 3.1.6
- Recursive arguments, 4.5.5
- Recursive Extraction, 22.1
- Recursive Extraction Library, 22.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
- Reserved Notation, 12.1.7
- Reset, 6.7.1
- Reset Extraction Inline, 22.2.2
- Reset Initial, 6.7.1
- Resource file, 14.3.1
- Restart, 7.2.2
- Restore State, 6.8.2
- red, 8.7.2
- refine, 8.2.3
- refl_identity, 3.1.3
- reflexivity, 8.6.4
- remember, 8.3.7
- rename, 8.3.6
- repeat, 9.2
- replace … with, 8.6.3
- rev, 3.2.5
- revert, 8.3.4
- revert dependent, 8.3.4
- rewrite, 8.6.1
- rewrite ->, 8.6.1
- rewrite <-, 8.6.1
- rewrite … at, 8.6.1
- rewrite … by, 8.6.1
- rewrite … in, 8.6.1
- right, 3.1.4, 8.2.6
- ring, 8.17.2, 24, 24.4
- ring_simplify, 8.17.2, 24.4
- rtauto, 8.10.3
- S, 3.1.3
- Save, 7.1.2
- Scheme, 13.1
- Scheme Equality, 13.1
- Schemes, 13.1
- 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
- Separate Extraction, 22.1
- Set, 6.2.1
- Set, 1.2.5, 4.1.1
- Set Automatic Coercions Import, 18.11
- Set Automatic Introduction, 7.4.3
- Set Contextual Implicit, 2.7.8
- Set Default Timeout, 6.9.5
- Set Elimination Schemes, 13.1.1
- Set Equality Schemes, 13.1.1
- Set Extraction AutoInline, 22.2.2
- Set Extraction KeepSingleton, 22.2.2
- Set Extraction Optimize, 22.2.2
- Set Firstorder Depth, 8.10.4
- 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 Parsing Explicit, 2.7.17
- Set Printing All, 2.9
- Set Printing Coercion, 18.8.2
- Set Printing Coercions, 18.8.1
- Set Printing Depth, 6.10.6
- Set Printing Existential Instances, 2.11.1
- Set Printing Implicit, 2.7.15
- Set Printing Implicit Defensive, 2.7.15
- 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.10.3
- Set Printing Wildcard, 2.2.4
- Set Reversible Pattern Implicit, 2.7.9
- Set Silent, 6.10.1
- Set Strict Implicit, 2.7.7
- Set Strongly Strict Implicit, 2.7.7
- Set Transparent Obligations, 23.2
- Set Virtual Machine, 6.11.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, 23.2
- Show Proof, 7.3.1
- Show Script, 7.3.1
- Show Tree, 7.3.1
- Show XML Proof, 15.5.5
- Silent mode, 6.10.1
- Solve Obligations, 23.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.11.3
- Structure, 18.9
- SubClass, 18.6.2
- Substitution, 4.1.3
- set, 8.3.7
- setoid_reflexivity, 26.7
- setoid_replace, 26, 26.7
- setoid_rewrite, 26.7
- setoid_symmetry, 26.7
- setoid_transitivity, 26.7
- sig, 3.1.4
- sig2, 3.1.4
- sigT, 3.1.4
- sigT2, 3.1.4
- simpl, 8.7.4
- simpl … in, 8.7.4
- simple apply, 8.2.4
- simple apply … in, 8.2.5
- simple destruct, 8.5.1
- simple eapply … in, 8.2.5
- simple induction, 8.5.2
- simple inversion, 8.5.8
- simple inversion … as, 8.5.8
- simplify_eq, 8.14.3
- snd, 3.1.3
- solve, 9.2
- sort, 1.2.1
- specialize, 8.4.1
- specif, 1.2.5
- split, 8.2.6
- split_Rabs, 3.2.4
- split_Rmult, 3.2.4
- stepl, 8.6.8
- stepr, 8.6.8
- string, 1.1
- subgoal, 8
- subst, 8.6.7
- sum, 3.1.3
- sumbool, 3.1.4
- sumor, 3.1.4
- sym_not_eq, 3.1.2
- symmetry, 8.6.5
- symmetry in, 8.6.5
- Tactic Definition, 8.18
- Tactic macros, 8.18
- Tactic Notation, 12.4
- 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
  - timeout, 9.2
  - try, 9.2
- Tactics, 8
- Terms, 1.2
- Test, 6.2.3
- Test Default Timeout, 6.9.7
- Test Ltac Debug, 9.4
- Test Printing Depth, 6.10.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.10.5
- Test Printing Wildcard, 2.2.4
- Test Virtual Machine, 6.11.7
- Test Whelp Getter, 6.3.11
- Test Whelp Server, 6.3.11
- Theorem, 1.3.5, 7.1
- Theories, 3
- Time, 6.9.3
- Timeout, 6.9.4
- Transparent, 6.11.2
- True, 3.1.2
- Type, 1.2.5, 4.1.1
- Type of constructor, 4.5.3
- Typeclasses eauto, 19.6.6
- Typeclasses Opaque, 19.6.5
- Typeclasses Transparent, 19.6.5
- Typing rules, 4.2
  - App, 4.2, 8.4.1
  - Ax, 4.2
  - Const, 4.2
  - Conv, 4.3, 8.3.1, 8.6.9
  - Fix, 4.5.5
  - Lam, 4.2, 8.3.1
  - Let, 4.2, 8.3.1
  - match, 4.5.4
  - Prod, 4.2
  - Prod (impredicative Set), 4.7
  - Var, 4.2
- tactic, 8.1
- tail, 3.2.5
- tauto, 8.10.1
- term, 1.2.1
- timeout, 9.2
- transitivity, 8.6.6
- trivial, 8.8.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.4
- Unfocused, 7.2.5
- Unset, 6.2.2
- Unset Automatic Coercions Import, 18.11
- Unset Automatic Introduction, 7.4.3
- Unset Contextual Implicit, 2.7.8
- Unset Default Timeout, 6.9.6
- Unset Extraction AutoInline, 22.2.2
- Unset Extraction KeepSingleton, 22.2.2
- Unset Extraction Optimize, 22.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 Parsing Explicit, 2.7.17
- Unset Printing All, 2.9
- Unset Printing Coercion, 18.8.2
- Unset Printing Coercions, 18.8.1
- Unset Printing Depth, 6.10.7
- Unset Printing Existential Instances, 2.11.1
- Unset Printing Implicit, 2.7.15
- Unset Printing Implicit Defensive, 2.7.15
- 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.10.4
- Unset Printing Wildcard, 2.2.4
- Unset Reversible Pattern Implicit, 2.7.9
- Unset Silent, 6.10.2
- Unset Strict Implicit, 2.7.7
- Unset Strongly Strict Implicit, 2.7.7
- Unset Virtual Machine, 6.11.6
- unfold, 8.7.5
- unfold … in, 8.7.5
- unify, 8.12.2
- unit, 3.1.3
- Variable, 1.3.1
- Variable (and coercions), 18.6.1
- Variables, 1.3.1
- value, 3.1.4
- vm_compute, 8.7.1, 8.7.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.8.1
- well_founded, 3.1.6
- XML exportation, 15.5
- ζ-reduction, 4.3, 4.3