is an extension to MetaOCaml with indexed types. Indexed types allow the programmer to express nested polymorphism as well as complex functional dependencies at the level of types. Small number of extensions to the term and type language are needed to give the user full access to the powerful Coq proof checker at the level of types. With these extensions, datatypes can be defined that reflect the size of a list or a vector in its type. Because Coq is one of the most expressive checkers available, any fact that can be proved in Coq can be used to give more refined types to programs. Because Coq propositions can be viewed as types, Concoqtion provides a natural way to incorporate formal verification techniques into programming practice. * Related Systems: Epigram, Cayenne, ATS, Omega, Elf and Twelf, RSP, DML, Harper and Licata's extension to DML, Lightwight dependent types, Attractive types, First Class Phantom Types, GADTs for Object-oriented languages, Scala