Systems based on versions of intensional type theory go back to the type-checker for the impredicative calculus of constructions which was written around 1984 by Coquand and Huet. This led to the Coq system, which is based on the calculus of inductive constructions (Paulin-Mohring 1993), a theory which extends the calculus of construction with primitive inductive types and families. The encodings of the pure calculus of constructions were found to be inconvenient, since the full elimination rules could not be derived and instead had to be postulated. We also remark that the calculus of inductive constructions has a subsystem, the predicative calculus of inductive constructions, which follows the principles of Martin-Löf’s intuitionistic type theory.