Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 115 insertions, 0 deletions

diff --git a/CREDITS b/CREDITS
new file mode 100644
index 00000000..12cd8e65
--- /dev/null
+++ b/CREDITS
@@ -0,0 +1,115 @@
+
+The "Coq proof assistant" was developed conjointly by 
+	INRIA Formel-Coq-LogiCal projects (since 1985), 
+	Laboratoire de l'Informatique du Parallelisme (LIP) 
+	associated to CNRS and ENS Lyon (Sep. 1989 to Aug. 1997),
+	Laboratoire de Recherche en Informatique (LRI)
+	associated to CNRS and Paris Sud (since Sep. 1997),
+	Laboratoire d'Informatique de l'Ecole Polytechnique (since Jan. 2003)
+	associated to CNRS and Ecole Polytechnique.
+
+All files of the "Coq proof assistant" in directories or sub-directories of
+	config dev doc interp kernel lib library parsing pretyping proofs
+	scripts syntax tactics test-suite theories tools toplevel translate
+are distributed under the terms of the GNU Lesser General Public License 
+Version 2.1 (see file LICENSE).
+These files are COPYRIGHT 1999-2004, The Coq development team, 
+CNRS, INRIA and Université Paris Sud
+
+
+The following directories contain independent contributions supported 
+by the Coq development team :
+contrib/cc
+	developed by Pierre Corbineau (ENS Cachan, 2001)
+contrib/correctness
+	developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
+contrib/extraction
+	developed by Pierre Letouzey (LRI, 2000-2004)
+contrib/field
+	developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
+contrib/first-order 
+	developed by Pierre Corbineau (LRI, 2003-2004)
+contrib/fourier
+	developed by Loïc Pottier (INRIA-Lemme, 2001)
+contrib/funind
+	developed by Pierre Courtieu (INRIA-Lemme, 2003-2004)
+contrib/interface
+	developed by Yves Bertot with contributions from Loïc Pottier and
+	Laurence Rideau as part of the Pcoq project (INRIA-Lemme, 1997-2004)
+contrib/jprover
+	The author of JProver is Stephan Schmitt <schmitts@spmail.slu.edu>,
+	and is integrated into MetaPRL by Aleksey Nogin <nogin@cs.cornell.edu>
+	and then into Coq by Guan-Shieng Huang (LRI, 2001-2002)
+	original files from Stephan Schmitt are "GPL"
+contrib/omega
+	developed by Pierre Crégut (France Telecom R&D, 1996)
+contrib/romega
+	developed by Pierre Crégut (France Telecom R&D, 2001-2004)
+contrib/ring
+	developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick 
+	Loiseleur (LRI, 1997-1999)
+contrib/xml
+	developed by Claudio Sacerdoti (Univ. Bologna, 2000-2004) 
+	as part of the HELM and MoWGLI project
+
+parsing/search.ml
+	developed by Yves Bertot (INRIA-Lemme, 2000-2004)
+theories/ZArith
+	started by Pierre Crégut (France Telecom R&D, 1996)
+ide/
+	developed by Benjamin Monate (LRI, 2003) with contributions 
+	from Claude Marché (INRIA, 2003-2004); some files from ide/utils 
+	come from Maxence Guesdon's Cameleon project and are "GPL"
+
+Many discussions within the Démons team and the LogiCal project
+influenced significantly the design of Coq especially with
+J. Courant, P. Courtieu, J. Duprat, J. Goubault,
+A. Miquel, C. Marché, B. Monate, B. Werner
+
+Intensive users suggested improvements of the system : 
+Y. Bertot, L. Pottier, L. Théry (INRIA-Lemme project) 
+C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D)
+P. Castéran (Université Bordeaux 1)
+
+The following people have contributed to the development of different versions 
+of the Coq Proof assistant during the indicated time :
+
+	Bruno Barras (INRIA, 1995-now)
+	Jacek Chrzaszcz (Paris Sud, 1998-2003)
+	Thierry Coquand (INRIA, 1985-1989)
+	Cristina Cornes (INRIA, 1993-1996)
+	Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996)
+	David Delahaye (INRIA, 1997-2002)
+	Daniel de Rauglaudre (INRIA, 1996-1998)
+	Olivier Desmettre (INRIA, 2001-2003)
+	Gilles Dowek (INRIA, 1991-1994)
+	Amy Felty (INRIA, 1993)
+	Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, Paris Sud, 1997-now)
+	Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998)
+	Hugo Herbelin (INRIA, 1996-now)
+	Gérard Huet (INRIA, 1985-1997)
+	Pierre Letouzey (LRI, 2000-now)
+	Pascal Manoury (INRIA, 1993)
+	Micaela Mayero (INRIA, 1997-2002)
+	Claude Marché (Paris Sud & INRIA, 2003-now)
+	César Muñoz (INRIA, 1994-1995)
+	Chetan Murthy (INRIA, 1992-1994)
+	Catherine Parent-Vigouroux (ENS Lyon, 1992-1995)
+	Patrick Loiseleur (Paris Sud, 1997-1999)
+	Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997, 
+				  Paris Sud, 1997-now)
+	Clément Renard (INRIA, 2001-now)
+	Amokrane Saïbi (INRIA, 1993-1998)
+	Benjamin Werner (INRIA, 1989-1994)
+
+
+***************************************************************************
+INRIA refers to :
+	Institut National de la Recherche en Informatique et Automatique
+CNRS refers to :
+	Centre National de la Recherche Scientifique
+Paris Sud refers to :
+	Université Paris Sud
+ENS Lyon refers to :
+	Ecole Normale Supérieure de Lyon
+****************************************************************************