The Coq proof assistant Copyright 1999-2015 The Coq development team, INRIA, CNRS, University Paris Sud, University Paris 7, Ecole Polytechnique. This product includes also software developed by Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega) Pierre Courtieu and Julien Forest, CNAM (plugins/funind) Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml) Pierre Corbineau, Radboud University, Nijmegen (declarative mode) John Harrison, University of Cambridge (csdp wrapper) The file CREDITS contains a list of contributors. The credits section in the Reference Manual details contributions.