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 »
Tactic Index

Tactic Index

a | f | l | s | u


	a
	`apply`
	`apply … in`

	f
	`fix`

	l
	`lapply`

	s
	`simple apply`
	`simple apply … in`

	u
	`unfold`

© Copyright 2016, Inria.

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