Chapter 2: Extensions of
Gallina
Gallina
is the kernel language of
Coq
. We describe here extensions of the Gallina's syntax.
2.1 Record types
2.2 Variants and extensions of
Cases
2.3 Forced type
2.4 Section mechanism
2.5 Logical paths of libraries and compilation units
2.6 Qualified names
2.7 Implicit arguments
2.8 Implicit Coercions