Coq
8.7

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 (full text)
  • 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 Objective Caml and Haskell
  • Program
  • The ring and field tactic families
  • Nsatz: tactics for proving equalities in integral domains
  • Generalized rewriting
  • Asynchronous and Parallel Proof Processing
  • Polymorphic Universes
  • Miscellaneous extensions
  • Coq glossary

Porting to Sphinx

  • The Gallina specification language
  • Calculus of Inductive Constructions
  • A subset of Coq's tactic reference
  • A few examples of trickier syntax constructs
Coq
  • Docs »
  • Option Index

Option Index

p | s | u
 
p
Printing Notations
 
s
Strict Universe Declaration.
 
u
Universal Lemma Under Conjunction
Universe Minimization ToSet
Universe Polymorphism

© Copyright 2016, Inria.

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