Global Index

# 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_equal` `i`, 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 tactic`1``;`tactic`2`, 9.2 tactic`0``;[`tactic`1``∣``…``∣`tactic`n``]`, 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