Part: I
The language

• Chapter 1: The Gallina specification language
• Chapter 2: Extensions of Gallina
• Chapter 3: The Coq library
• Chapter 4: The Calculus of Inductive Constructions