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
»
Index
Index
Symbols
|
A
|
B
|
C
|
D
|
E
|
F
|
G
|
I
|
L
|
M
|
N
|
O
|
P
|
R
|
S
|
T
|
U
|
V
|
Β
|
Symbols
Symbols
`qualid` is not a module (error)
A
Add Printing Constructor ‘ident’. (command)
Add Printing If ‘ident’. (command)
Add Printing Let ‘ident’. (command)
Add Printing Record ‘ident’. (command)
apply (tactic notation)
apply … in (tactic notation)
Arguments ‘qualid’ : clear implicits. (command)
Arguments ‘qualid’ : clear scopes (command)
Arguments ‘qualid’ : default implicits. (command)
Arguments ‘qualid’ ‘name’ : ‘rename’. (command)
Arguments ‘qualid’ ‘name’%‘scope’…‘name’%‘scope’ (command)
Arguments ‘qualid’ ‘possibly_bracketed_ident’. (command)
B
bad occurrence number of ‘qualid’ (error)
Bind Scope ‘scope’ with ‘qualid’ (command)
C
Cannot build functional inversion principle (warn)
Cannot define graph for ‘ident’ (warn)
Cannot define principle(s) for ‘ident’ (warn)
Cannot handle mutually (co)inductive records. (error)
Cannot infer a term for this placeholder. (error)
Cannot use mutual definition with well-founded recursion or measure (error)
Canonical Structure ‘ident’ : ‘type’ := ‘term’. (command variant)
Canonical Structure ‘ident’ := ‘term’ : ‘type’. (command variant)
Canonical Structure ‘ident’ := ‘term’. (command variant)
Canonical Structure ‘qualid’. (command)
Close Scope ‘scope’ (command)
Coercion ‘qualid’ : ‘class’ >-> ‘class’. (command)
Constraint ‘ident’ ‘ord’ ‘ident’. (command)
D
Declare Module ‘ident’ : ‘module_type’. (command)
Declare Module ‘ident’ ‘module_binding’ : ‘module_type’. (command variant)
Delimit Scope ‘scope’ with ‘ident’ (command)
E
Either there is a type incompatibility or the problem involves dependencies (error)
End ‘ident’. (command)
,
[1]
,
[2]
Export ‘qualid’ (command variant)
F
fix (tactic notation)
Function ‘ident’ ‘binder’ : ‘type’ := ‘term’ (command variant)
Function ‘ident’ ‘binder’ { measure ‘term’ ‘ident’ } : ‘type’ := ‘term’ (command variant)
Function ‘ident’ ‘binder’ { struct ‘ident’ } : ‘type’ := ‘term’ (command variant)
Function ‘ident’ ‘binder’ { wf ‘term’ ‘ident’ } : ‘type’ := ‘term’ (command variant)
Function ‘ident’ ‘binder’ { ‘decrease_annot’ } : ‘type’ := ‘term’. (command)
G
Generalizable (Variable | Variables) ‘ident’…‘ident’. (command)
Generalizable All Variables. (command)
Generalizable No Variables. (command)
Global Arguments ‘qualid’ : default implicits (command variant)
Global Arguments ‘qualid’ ‘name’%‘scope’…‘name’%‘scope’ (command variant)
Global Arguments ‘qualid’ ‘possibly_bracketed_ident’ (command variant)
Global Close Scope ‘scope’. (command)
Global Generalizable. (command)
Global Open Scope ‘scope’. (command)
Global | Local Arguments ‘qualid’ ‘possibly_bracketed_ident’…‘possibly_bracketed_ident’. (command variant)
I
Implicit Type ‘ident’ : ‘type’. (command variant)
Implicit Types ( ‘ident’…‘ident’ : ‘term’ )…( ‘ident’…‘ident’ : ‘term’ ) (command variant)
Implicit Types ‘ident’…‘ident’ : ‘type’. (command)
Import ‘qualid’. (command)
Impossible to unify … with … (error)
Include ‘module’. (command)
,
[1]
Include ‘module’<+ …<+ ‘module’. (command)
,
[1]
Infix "‘symbol’" := ‘qualid’ (‘modifier’, …, ‘modifier’). (command)
L
lapply (tactic variant)
Local Arguments ‘qualid’ : default implicits (command variant)
Local Arguments ‘qualid’ ‘name’%‘scope’…‘name’%‘scope’ (command variant)
Local Arguments ‘qualid’ ‘possibly_bracketed_ident’. (command variant)
Local Close Scope ‘scope’. (command)
Local Notation ‘ident’ ‘ident’…‘ident’ := ‘term’ (only parsing). (command)
Local Notation ‘notation’ (command)
Local Open Scope ‘scope’. (command)
Local Tactic Notation (at level ‘level’) ‘prod_item’…‘prod_item’ := ‘tactic’. (command)
Local Tactic Notation (command variant)
Locate Module ‘qualid’. (command)
Locate ‘symbol’ (command)
M
Module [ Import | Export ]. (command variant)
Module Type ‘ident’ := ‘module_type’. (command)
Module Type ‘ident’ ‘module_binding’ := ‘module_type’. (command variant)
Module Type ‘ident’ ‘module_binding’ := ‘module_type’<+ …<+ ‘module_type’. (command variant)
Module Type ‘ident’ ‘module_binding’. (command variant)
Module Type ‘ident’. (command)
Module ‘ident’ : ‘module_type’. (command variant)
Module ‘ident’ := ‘module_expression’. (command)
Module ‘ident’ <: ‘module_type’<: …<: ‘module_type’. (command variant)
Module ‘ident’ ‘module_binding’ : ‘module_type’ := ‘module_expression’. (command variant)
Module ‘ident’ ‘module_binding’ : ‘module_type’. (command variant)
Module ‘ident’ ‘module_binding’ := ‘module_expression’. (command variant)
Module ‘ident’ ‘module_binding’ := ‘module_expression’<+ …<+ ‘module_expression’. (command variant)
Module ‘ident’ ‘module_binding’ <: ‘module_type’<
…<; ‘module_type’. (command variant)
Module ‘ident’ ‘module_binding’ <: ‘module_type’<: …<: ‘module_type’ := ‘module_expression’. (command variant)
Module ‘ident’ ‘module_binding’. (command variant)
Module ‘ident’. (command)
Monomorphic ‘definition’ (command)
N
No argument name ‘ident’ (error)
No such label ‘ident’ (error)
Non exhaustive pattern-matching (error)
Not the right number of missing arguments (error)
O
Open Scope ‘scope’ (command)
P
Polymorphic ‘definition’ (command)
Print Grammar constr. (command)
Print Grammar pattern. (command)
Print Grammar tactic (command)
Print Implicit ‘qualid’. (command)
Print Module Type ‘ident’. (command)
Print Module ‘ident’. (command)
Print Scope scope (command variant)
Print Scopes (command variant)
Print Sorted Universes ‘string’. (command)
Print Sorted Universes. (command)
Print Table Printing If. (command)
Print Table Printing Let. (command)
Print Visibility (command)
Print Visibility scope (command variant)
Printing Notations (option)
R
Record ‘ident’ ‘param’ : ‘sort’ := ‘ident’ { ‘ident’ ‘binder’ : ‘term’ }. (command)
Records declared with the keyword Record or Structure cannot be recursive. (error)
Remove Printing If ‘ident’. (command)
Remove Printing Let ‘ident’. (command)
S
Section ‘ident’. (command)
Set Contextual Implicit. (command)
Set Implicit Arguments. (command)
Set Maximal Implicit Insertion. (command)
Set Parsing Explicit. (command)
Set Printing All. (command)
Set Printing Existential Instances. (command)
Set Printing Implicit Defensive. (command)
Set Printing Implicit. (command)
Set Printing Matching. (command)
Set Printing Projections. (command)
Set Printing Synth. (command)
Set Printing Universes. (command)
Set Printing Wildcard. (command)
Set Reversible Pattern Implicit. (command)
Set Strongly Strict Implicit. (command)
Signature components for label ‘ident’ do not match (error)
simple apply (tactic variant)
simple apply … in (tactic variant)
Statement without assumptions (error)
Strict Universe Declaration. (option)
T
Test Printing If for ‘ident’. (command)
Test Printing Let for ‘ident’. (command)
Test Printing Matching. (command)
Test Printing Synth. (command)
Test Printing Wildcard. (command)
The constructor ‘ident’ expects ‘num’ arguments (error)
The elimination predicate term should be of arity ‘num’ (for non dependent case) or ‘num’ (for dependent case) (error)
The recursive argument must be specified (error)
This is not the last opened module (error)
This is not the last opened module type (error)
This is not the last opened section (error)
Trying to mask the absolute name `qualid` ! (warn)
U
Unable to apply (error)
Unable to find an instance for the variables ‘ident’…‘ident’ (error)
Unable to infer a match predicate (error)
Undeclared universe ‘ident’. (error)
Undelimit Scope ‘scope’ (command)
unfold (tactic notation)
Universal Lemma Under Conjunction (option)
Universe inconsistency. (error)
Universe Minimization ToSet (option)
Universe Polymorphism (option)
Universe ‘ident’. (command)
Unset Maximal Implicit Insertion. (command)
Unset Parsing Explicit. (command)
Unset Printing All. (command)
Unset Printing Existential Instances. (command)
Unset Printing Implicit Defensive. (command)
Unset Printing Implicit. (command)
Unset Printing Matching. (command)
Unset Printing Records. (command)
Unset Printing Synth. (command)
Unset Printing Universes. (command)
Unset Printing Wildcard. (command)
Unset Strict Implicit. (command)
V
Variant ‘ident’ ‘params’ : ‘sort’ := ‘ident’ (‘ident’ : ‘term_1’). (command)
Β
βι normal form
Symbols
‘assumption_keyword’ Inline ‘assums’. (command)
‘ident’ cannot be defined. (warn)
‘qualid’ does not denote an evaluable constant (error)
‘qualid’ does not occur (error)