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 States and Reset
- 6.8 Quitting and debugging
- 6.9 Controlling display
- 6.10 Controlling the reduction strategies and the conversion algorithm
- 6.11 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 13 The Coq commands
- Chapter 14 Utilities
- 14.1 Building a toplevel extended with user tactics
- 14.2 Modules dependencies
- 14.3 Creating a Makefile for Coq modules
- 14.4 Documenting Coq files with coqdoc
- 14.5 Exporting Coq theories to XML
- 14.6 Embedded Coq phrases inside LATEX documents
- 14.7 Coq and GNU Emacs
- 14.8 Module specification
- 14.9 Man pages
- Chapter 15 Coq Integrated Development Environment
- 15.1 Managing files and buffers, basic edition
- 15.2 Interactive navigation into Coq scripts
- 15.3 Try tactics automatically
- 15.4 Proof folding
- 15.5 Vernacular commands, templates
- 15.6 Queries
- 15.7 Compilation
- 15.8 Customizations
- 15.9 Using unicode symbols
- 15.10 Building a custom CoqIDE with user ML code
Part V |
- Presentation of the Addendum
- Chapter 16 Extended pattern-matching
- Chapter 17 Implicit Coercions
- 17.1 General Presentation
- 17.2 Classes
- 17.3 Coercions
- 17.4 Identity Coercions
- 17.5 Inheritance Graph
- 17.6 Declaration of Coercions
- 17.7 Displaying Available Coercions
- 17.8 Activating the Printing of Coercions
- 17.9 Classes as Records
- 17.10 Coercions and Sections
- 17.11 Coercions and Modules
- 17.12 Examples
- Chapter 18 Type Classes
- Chapter 19 Omega: a solver of quantifier-free problems in Presburger Arithmetic
- Chapter 20 Micromega : tactics for solving arithmetics goals over ordered rings
- Chapter 21 Extraction of programs in Objective Caml and Haskell
- Chapter 22 Program
- Chapter 23 The ring and field tactic families
- Chapter 24 Nsatz: tactics for proving equalities in integral domains
- Chapter 25 User defined equalities and relations
- 25.1 Relations and morphisms
- 25.2 Adding new relations and morphisms
- 25.3 Rewriting and non reflexive relations
- 25.4 Rewriting and non symmetric relations
- 25.5 Rewriting in ambiguous setoid contexts
- 25.6 First class setoids and morphisms
- 25.7 Tactics enabled on user provided relations
- 25.8 Printing relations and morphisms
- 25.9 Deprecated syntax and backward incompatibilities
- 25.10 Rewriting under binders
- 25.11 Sub-relations
- 25.12 Constant unfolding
- References
- Global Index
- Tactics Index
- Vernacular Commands Index
- Index of Error Messages