Vernacular Commands Index

# Coq Reference Manual

# Vernacular Commands Index

`Abort`, 7.1.5 `About`, 6.1.1 `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 `Axiom`, 1.3.1 `Axiom` (and coercions), 17.6.1 `Back`, 6.7.2 `BackTo`, 6.7.3 `Backtrack`, 6.7.3 `Bind Scope`, 12.2.2 `Canonical Structure`, 2.7.15 `Cd`, 6.6.2 `Check`, 6.3.1 `Class`, 18.6.1 `Close Scope`, 12.2.1 `Coercion`, 2.8, 17.6.1, 17.6.1 `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 `Compute`, 6.3.3 `Conjecture`, 1.3.1 `Context`, 18.6.4 `Corollary`, 1.3.5 `CreateHintDb`, 8.13.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 `Delimit Scope`, 12.2.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 `Drop`, 6.8.2 `End`, 2.4.2, 2.5.2, 2.5.5 `Eval`, 6.3.2 `Example`, 1.3.2 `Existential`, 7.1.8 `Existing Class`, 18.6.1 `Existing Instance`, 18.6.3 `Export`, 2.5.8 `Extract Constant`, 21.2.4 `Extract Inductive`, 21.2.4 `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 `Fact`, 1.3.5 `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 `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 `Guarded`, 7.3.2 `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 `Hypotheses`, 1.3.1 `Hypothesis`, 1.3.1 `Hypothesis` (and coercions), 17.6.1 `Identity Coercion`, 17.6.2 `Implicit Arguments`, 2.7.4, 2.7.5 `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 `Infix`, 12.1.6 `Inline`, 2.5.4 `Inspect`, 6.1.2 `Instance`, 18.6.2 `Lemma`, 1.3.5 `Let`, 1.3.2 `Load`, 6.4.1 `Load Verbose`, 6.4.1 `Local`, 6.11.1 `Local Coercion`, 17.6.1, 17.6.1 `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 `Ltac`, 9.3 `Module`, 2.5.1, 2.5.3 `Module Type`, 2.5.4 `Next Obligation`, 22.2 `Notation`, 12.1, 12.3 `Obligation`, 22.2 `Obligation Tactic`, 22.2 `Obligations`, 22.2 `Opaque`, 6.10.1 `Open Scope`, 12.2.1 `Parameter`, 1.3.1 `Parameter` (and coercions), 17.6.1 `Parameters`, 1.3.1 `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 Definition`, 22.1.1 `Program Fixpoint`, 22.1.2 `Program Instance`, 18.1, 18.6.2 `Program Lemma`, 22.1.3 `Proof`, 1.3.5, 7.1.4 `Proof with`, 8.13.6 `Proposition`, 1.3.5 `Pwd`, 6.6.1 `Qed`, 1.3.5, 7.1.2 `Quit`, 6.8.1 `Record`, 2.1 `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 `Restart`, 7.2.4 `Restore State`, 6.7.4 `Resume`, 7.1.7 `Save`, 7.1.2 `Scheme`, 8.14, 10.3 `Scheme Equality`, 8.14 `Search`, 6.3.6 `SearchAbout`, 6.3.7 `SearchPattern`, 6.3.8 `SearchRewrite`, 6.3.9 `Section`, 2.4.1 `Set`, 6.2.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 `Solve Obligations`, 22.2 `Strategy`, 6.10.3 `Structure`, 17.9 `SubClass`, 17.6.2 `Suspend`, 7.1.6 `setoid_reflexivity`, 25.7 `setoid_replace`, 25.7 `setoid_rewrite`, 25.7 `setoid_symmetry`, 25.7 `setoid_transitivity`, 25.7 `Tactic Definition`, 8.16 `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 `Time`, 6.8.3 `Timeout`, 6.8.4 `Transparent`, 6.10.2 `Typeclasses eauto`, 18.6.6 `Typeclasses Opaque`, 18.6.5 `Typeclasses Transparent`, 18.6.5 `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 `Variable`, 1.3.1 `Variable` (and coercions), 17.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.7.5