Part I |
- Chapter 1 The Gallina specification language
- Chapter 2 Extensions of Gallina
- Chapter 3 The Coq library
- Chapter 4 Calculus of Inductive Constructions
- Chapter 5 The Module System
Part II |
- Chapter 6 Vernacular commands
- 6.1 Displaying
- 6.2 Options and Flags
- 6.3 Requests to the environment
- 6.4 Loading files
- 6.5 Compiled files
- 6.6 Loadpath
- 6.7 Backtracking
- 6.8 State files
- 6.9 Quitting and debugging
- 6.10 Controlling display
- 6.11 Controlling the reduction strategies and the conversion algorithm
- 6.12 Controlling the locality of commands
- Chapter 7 Proof handling
- Chapter 8 Tactics
- 8.1 Invocation of tactics
- 8.2 Explicit proof as a term
- 8.3 Basics
- 8.4 Negation and contradiction
- 8.5 Conversion tactics
- 8.6 Introductions
- 8.7 Induction and Case Analysis
- 8.8 Equality
- 8.9 Equality and inductive sets
- 8.10 Inversion
- 8.11 Classical tactics
- 8.12 Automatizing
- 8.13 Controlling automation
- 8.14 Generation of induction principles with Scheme
- 8.15 Generation of induction principles with Functional Scheme
- 8.16 Simple tactic macros
- Chapter 9 The tactic language
- Chapter 10 Detailed examples of tactics
- Chapter 11 The Mathematical Proof Language
Part III |
Part IV |
- Chapter 14 The Coq commands
- Chapter 15 Utilities
- 15.1 Building a toplevel extended with user tactics
- 15.2 Modules dependencies
- 15.3 Creating a Makefile for Coq modules
- 15.4 Documenting Coq files with coqdoc
- 15.5 Exporting Coq theories to XML
- 15.6 Embedded Coq phrases inside LATEX documents
- 15.7 Coq and GNU Emacs
- 15.8 Module specification
- 15.9 Man pages
- Chapter 16 Coq Integrated Development Environment
Part V |
- Presentation of the Addendum
- Chapter 17 Extended pattern-matching
- Chapter 18 Implicit Coercions
- 18.1 General Presentation
- 18.2 Classes
- 18.3 Coercions
- 18.4 Identity Coercions
- 18.5 Inheritance Graph
- 18.6 Declaration of Coercions
- 18.7 Displaying Available Coercions
- 18.8 Activating the Printing of Coercions
- 18.9 Classes as Records
- 18.10 Coercions and Sections
- 18.11 Coercions and Modules
- 18.12 Examples
- Chapter 19 Type Classes
- Chapter 20 Omega: a solver of quantifier-free problems in Presburger Arithmetic
- Chapter 21 Micromega : tactics for solving arithmetic goals over ordered rings
- 21.1 Short description of the tactics
- 21.2 Positivstellensatz refutations
- 21.3 lra : a decision procedure for linear real and rational arithmetic
- 21.4 psatz : a proof procedure for non-linear arithmetic
- 21.5 lia : a tactic for linear integer arithmetic
- 21.6 nia : a proof procedure for non-linear integer arithmetic
- Chapter 22 Extraction of programs in Objective Caml and Haskell
- Chapter 23 Program
- Chapter 24 The ring and field tactic families
- Chapter 25 Nsatz: tactics for proving equalities in integral domains
- Chapter 26 User defined equalities and relations
- 26.1 Relations and morphisms
- 26.2 Adding new relations and morphisms
- 26.3 Rewriting and non reflexive relations
- 26.4 Rewriting and non symmetric relations
- 26.5 Rewriting in ambiguous setoid contexts
- 26.6 First class setoids and morphisms
- 26.7 Tactics enabled on user provided relations
- 26.8 Printing relations and morphisms
- 26.9 Deprecated syntax and backward incompatibilities
- 26.10 Rewriting under binders
- 26.11 Sub-relations
- 26.12 Constant unfolding
- References
- Global Index
- Tactics Index
- Vernacular Commands Index
- Index of Error Messages