This package was debianized by Fernando Sanchez <fer@debian.org>

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.