Mise a jour CREDITS en vue copyright

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5490 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 26 insertions, 27 deletions

diff --git a/CREDITS b/CREDITS
index ad186afb3..beb9dabbe 100644
--- a/CREDITS
+++ b/CREDITS
@@ -4,58 +4,55 @@ The "Coq proof assistant" was developed conjointly by
 	Laboratoire de l'Informatique du Parallelisme (LIP) 
 	associated to CNRS and ENS Lyon (sept.89-sept.97),
 	Laboratoire de Recherche en Informatique (LRI)
-	associated to CNRS and Paris 11 (since sept. 97).
+	associated to CNRS and Paris Sud (since sept. 97),
+	Laboratoire d'Informatique de l'Ecole Polytechnique (since jan 03)
+	associated to CNRS and Ecole Polytechnique.
 
 All files of the "Coq proof assistant" in directories or sub-directories of
 	config contrib dev doc kernel lib library parsing pretyping 
 	proofs scripts syntax tactics test-suite theories tools toplevel
 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 current version V7 is a new implementation started in september 1999.
-  	J-C. Filliâtre designed the architecture of the new system, a
-new represention of environments and wrote a new kernel for
-type-checking terms (LRI)
-        H. Herbelin introduced a new structure of terms with local
-definitions. He introduced ``qualified'' names, wrote a new
-pattern-matching compilation algorithm and designed an
-algebraic structure for universes (INRIA)
-	D. Delahaye introduced a new language for tactics (INRIA)
-	B. Barras improved the reduction strategy for lazy evaluation (INRIA)
-	P. Letouzey redesigned the extraction mechanism from proofs 
-to functional programs (LRI)
 
 The following directories contain independant contributions supported 
-by the Coq development team for the new architecture :
+by the Coq development team :
 contrib/correctness
 	developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
 contrib/extraction
 	developed by Pierre Letouzey (LRI, 2000-2001)
 contrib/field
 	developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
+contrib/first-order 
+	developed by Pierre Corbineau (Paris Sud, 2003-2004)
 contrib/fourier
 	developed by Loic Pottier (INRIA-Lemme, 2001)
+contrib/funind
+	developed by P. Courtieu (INRIA-Lemme, 2003-2004)
 contrib/interface
 	developed by Yves Bertot (INRIA-Lemme, 1997)
+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)
 contrib/omega
-	developed by Pierre Cregut (France Telecom R&D, 1996)
+	developed by Pierre Crégut (France Telecom R&D, 1996)
 contrib/romega
-	developed by Pierre Cregut (France Telecom R&D, 2001)
+	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 Sacerdotti (Univ. Bologna, 2000-2001)
-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 HUANG Guan-Shieng (LRI, 2001-2002)
+
 parsing/search.ml
 	developed by Yves Bertot (INRIA-Lemme, 2000)
 
 Many discussions within the Démons team and the LogiCal project
 influenced significantly the design of Coq especially with
-J. Chrzaszcz, J. Courant, P. Courtieu, J. Duprat, J. Goubault,
+J. Courant, P. Courtieu, J. Duprat, J. Goubault,
 A. Miquel, C. Marché, B. Monate, B. Werner
 
 Intensive users suggested improvements of the system : 
@@ -66,27 +63,29 @@ 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-now)
+	David Delahaye,  (INRIA, 1997-2001)
 	Daniel de Rauglaudre, (INRIA, 1996-1998)
-        Olivier Desmettre (INRIA, 2001-now)
+        Olivier Desmettre (INRIA, 2001-2002)
 	Gilles Dowek, (INRIA, 1991-1994)
 	Amy Felty, (INRIA, 1993)
-	Jean-Christophe Filliâtre, (ENS Lyon, 1994-1997) (Paris 11,1997-now)
+	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-now)
+	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 11, 1997-1999)
+	Patrick Loiseleur, (Paris Sud, 1997-1999)
   	Christine Paulin-Mohring, (INRIA, 1985-1989) (ENS Lyon, 1989-1997) 
-				  (Paris 11, 1997-now)
+				  (Paris Sud, 1997-now)
         Clément Renard, (INRIA, 2001-now)
 	Amokrane Saïbi, (INRIA, 1993-1998)
 	Benjamin Werner, (INRIA, 1989-1994)
@@ -97,7 +96,7 @@ INRIA refers to :
 	Institute National de la Recherche en Informatique et Automatique
 CNRS refers to :
 	Centre National de la Recherche Scientifique
-Paris 11 refers to :
+Paris Sud refers to :
 	Universite Paris Sud
 ENS Lyon refers to :
 	Ecole Normale Superieure de Lyon