Coq
8.8.2

Indexes

  • Index
  • Command index
  • Tactic index
  • Flags, options and tables index
  • Errors and warnings index

Preamble

  • Introduction
  • Credits

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
  • The tactic language
  • Detailed examples of tactics
  • The SSReflect proof language

User extensions

  • Syntax extensions and interpretation scopes
  • Proof schemes

Practical tools

  • The Coq commands
  • Utilities
  • Coq Integrated Development Environment

Addendum

  • Extended pattern matching
  • Implicit Coercions
  • Canonical Structures
  • Type Classes
  • Omega: a solver for quantifier-free problems in Presburger Arithmetic
  • Micromega: tactics for solving arithmetic goals over ordered rings
  • Extraction of programs in OCaml and Haskell
  • Program
  • The ring and field tactic families
  • Nsatz: tactics for proving equalities in integral domains
  • Generalized rewriting
  • Asynchronous and Parallel Proof Processing
  • Miscellaneous extensions
  • Polymorphic Universes

Reference

  • Bibliography
Coq
  • Docs »
  • Search

© Copyright 1999-2018, Inria.

Built with Sphinx using a theme provided by Read the Docs.