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 Local definitions
2.5 Section mechanism
2.6 Implicit arguments
2.7 Implicit Coercions
