The Coq proof assistant has been developed at INRIA, Ecole Normale Superieure de Lyon, and University of Paris South for more than twenty years [6]. Its theoretical foundation is known as the "Calculus of Inductive Constructions" [4,5]. Versions of the system were distributed regularly from 1989 (version 4.10). The current revision is 8.1 and a revision 8.2 is about to come out. This 8th generation was started in 2004, at the time when a radical change in syntax was enforced and a textbook [2] was published. A more complete historical overview, provided by G. Huet and C. Paulin-Mohring, is available in the book foreword. The calculus of Inductive constructions is a variant of typed lambda-calculus based on dependent types. Theorems are directly represented by terms of the lambda-calculus, in the same language that is also used to describe formulas and programs. Having all elements of the logic at the same level makes it possible to mix computation and theorem proving in productive ways.