This package was debianized by Fernando Sanchez It was downloaded from ftp://ftp.inria.fr/INRIA/LogiCal/coq/current The Coq proof assistant V7 and V8 includes software developed by the Coq development team inside the LogiCal project, at INRIA, CNRS and University Paris Sud. Copyright 1999-2005 The Coq development team, INRIA-CNRS, University Paris Sud, All rights reserved. This product includes also software developed by Yves Bertot, Lemme, INRIA Sophia-Antipolis (contrib/interface, parsing/search.ml) Pierre Crégut, France Telecom R & D (contrib/omega and contrib/romega) Pierre Courtieu, Lemme (contrib/funind) Loïc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier) Claudio Sacerdoti Coen, HELM, University of Bologna (contrib/xml) Coq includes a tactic Jp based on JProver, a theorem prover for first-order intuitionistic logic. Jprover was originally implemented by Stephan Schmitt and then integrated into MetaPRL by Aleksey Nogin. After this, Huang extracted the necessary ML-codes from MetaPRL and then integrated it into Coq. The Coq development Team (march 2004) Bruno Barras (INRIA) Pierre Corbineau (Université Paris Sud) Jean-Christophe Filliâtre (CNRS) Hugo Herbelin (INRIA) Pierre Letouzey (Université Paris Sud) Claude Marché (Université Paris Sud-INRIA) Christine Paulin (Université Paris Sud) Clément Renard (INRIA) The complete list of developpers and contributors can be found in /usr/share/doc/doc/CREDITS.gz Copyright: the Coq Proof Assistant is distributed under the terms of the GNU Lesser General Public Licence, version 2.1, see /usr/share/common-licenses/LGPL-2.1. However there are two exceptions: files in the directories contrib/jprover and ide/utils are distributed under the terms of the GNU General Public Licence, see /usr/share/common-licenses/GPL-2.