The language

- The Gallina specification language
- Extensions of Gallina
- The Coq library
- Calculus of Inductive Constructions
- The Module System

The proof engine

- Vernacular commands
- Proof handling
- Tactics
- Invocation of tactics
- Explicit proof as a term
- Basics
- Negation and contradiction
- Conversion tactics
- Introductions
- Eliminations (Induction and Case Analysis)
- Equality
- Equality and inductive sets
- Inversion
- Automatizing
- The hints databases for
`auto`and`eauto` - Generation of induction principles with
`Scheme` - Generation of induction principles with
`Functional Scheme` - Simple tactic macros

- The tactic language
- Detailed examples of tactics

User extensions

Practical tools

Addendum to the Reference Manual

- Presentation of the Addendum
- Extended pattern-matching
- Implicit Coercions
- Omega: a solver of quantifier-free problems in Presburger Arithmetic
- Extraction of programs in Objective Caml and Haskell
- The
`ring`tactic - The
`setoid_replace`tactic - References
- Global Index
- Tactics Index
- Vernacular Commands Index
- Index of Error Messages

This document was translated from L^{A}T_{E}X by H^{E}V^{E}A and H^{A}C^{H}A.