# Coq Reference Manual

# Vernacular Commands Index

- * (command), 7.2.7
- + (command), 7.2.7
- - (command), 7.2.7
- {, 7.2.6
- }, 7.2.6
- Abort, 7.1.6
- About, 6.1.1
- 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
- Axiom, 1.3.1
- Axiom (and coercions), 18.6.1
- Back, 6.7.2
- BackTo, 6.7.3
- Backtrack, 6.7.3
- Bind Scope, 12.2.2
- Canonical Structure, 2.7.18
- Cd, 6.6.2
- Check, 6.3.1
- Class, 19.6.1
- Close Scope, 12.2.1
- Coercion, 2.8, 18.6.1, 18.6.1
- 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
- Compute, 6.3.3
- Conjecture, 1.3.1
- Context, 19.6.4
- Corollary, 1.3.5
- CreateHintDb, 8.9.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
- Delimit Scope, 12.2.2
- Derive Dependent Inversion, 13.3
- Derive Dependent Inversion_clear, 13.3
- Derive Inversion, 13.3
- Derive Inversion_clear, 13.3
- Drop, 6.9.2
- End, 2.4.2, 2.5.2, 2.5.5
- Eval, 6.3.2
- Example, 1.3.2
- Existential, 7.1.7
- Existing Class, 19.6.1
- Existing Instance, 19.6.3
- Existing Instances, 19.6.3
- Export, 2.5.8
- Extract Constant, 22.2.4
- Extract Inductive, 22.2.4
- 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
- Fact, 1.3.5
- Fixpoint, 1.3.4, 1.3.5
- Fixpoint … where …, 12.1.8
- Focus, 7.2.3
- Function, 2.3
- Functional Scheme, 13.2
- 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
- Grab Existential Variables, 7.1.8
- Guarded, 7.3.2
- 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
- Hypotheses, 1.3.1
- Hypothesis, 1.3.1
- Hypothesis (and coercions), 18.6.1
- Identity Coercion, 18.6.2
- Implicit Arguments, 2.7.13
- 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
- Infix, 12.1.6
- Inline, 2.5.4
- Inspect, 6.1.2
- Instance, 19.6.2
- Lemma, 1.3.5
- Let, 1.3.2
- Load, 6.4.1
- Load Verbose, 6.4.1
- Local, 6.12.1
- Local Arguments, 2.7.4, 2.7.5
- Local Coercion, 18.6.1, 18.6.1
- 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
- Ltac, 9.3
- Module, 2.5.1, 2.5.3
- Module Type, 2.5.4
- Next Obligation, 23.2
- Notation, 12.1, 12.3
- Obligation, 23.2
- Obligation Tactic, 23.2
- Obligations, 23.2
- Opaque, 6.11.1
- Open Scope, 12.2.1
- Parameter, 1.3.1
- Parameter (and coercions), 18.6.1
- Parameters, 1.3.1
- 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 Definition, 23.1.2
- Program Fixpoint, 23.1.3
- Program Instance, 19.1, 19.6.2
- Program Lemma, 23.1.4
- Proof, 1.3.5, 7.1.4
- Proof using, 7.1.5
- Proof with, 8.9.6
- Proposition, 1.3.5
- Pwd, 6.6.1
- Qed, 1.3.5, 7.1.2
- Quit, 6.9.1
- Record, 2.1
- 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
- Restart, 7.2.2
- Restore State, 6.8.2
- Save, 7.1.2
- Scheme, 13.1
- Scheme Equality, 13.1
- Search, 6.3.6
- SearchAbout, 6.3.7
- SearchPattern, 6.3.8
- SearchRewrite, 6.3.9
- Section, 2.4.1
- Separate Extraction, 22.1
- Set, 6.2.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
- Solve Obligations, 23.2
- Strategy, 6.11.3
- Structure, 18.9
- SubClass, 18.6.2
- setoid_reflexivity, 26.7
- setoid_replace, 26.7
- setoid_rewrite, 26.7
- setoid_symmetry, 26.7
- setoid_transitivity, 26.7
- Tactic Definition, 8.18
- Tactic Notation, 12.4
- 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
- Time, 6.9.3
- Timeout, 6.9.4
- Transparent, 6.11.2
- Typeclasses eauto, 19.6.6
- Typeclasses Opaque, 19.6.5
- Typeclasses Transparent, 19.6.5
- 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
- Variable, 1.3.1
- Variable (and coercions), 18.6.1
- Variables, 1.3.1
- 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