Mise a jour

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

1 files changed, 33 insertions, 17 deletions

diff --git a/CREDITS b/CREDITS
index affa2f30d..fde4b2b98 100644
--- a/CREDITS
+++ b/CREDITS
@@ -13,30 +13,45 @@ are distributed under the terms of the GNU Lesser General Public License
 Version 2.1 (see file LICENSE).
 
 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 and redesigned 
-the translation from the high-level language of Coq to the internal representation (INRIA)
+  	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 and redesigned the translation from the high-level
+language of Coq to the internal representation (INRIA)
 	D. Delahaye introduced a new language for tactics (INRIA)
 	B. Barras improved the reduction strategy for lazy evaluation (INRIA)
-The development was coordinated by C. Paulin (LRI).
+	P. Letouzey redesigned the extraction mechanism from proofs 
+to functional programs
 
 The following directories contain independant contributions supported 
 by the Coq development team for the new architecture :
+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/fourier
+	developed by Loic Pottier (INRIA-Lemme, 2001)
+contrib/interface
+	developed by Yves Bertot (INRIA-Lemme, 1997)
 contrib/omega
 	developed by Pierre Cregut (France Telecom R&D, 1996)
+contrib/romega
+	developed by Pierre Cregut (France Telecom R&D, 2001)
 contrib/ring
-	developed by Samuel Boutin (INRIA, 1996)
+	developed by Samuel Boutin (INRIA-Coq, 1996)
 	          and Patrick Loiseleur (LRI, 1997-1999)
 contrib/xml
 	developed by Claudio Sacerdotti (Univ. Bologna, 2000-2001)
 parsing/search.ml
-	developed by Yves Bertot (INRIA, 2000)
+	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, A. Miquel, C. Marché, 
-M. Mayero, B. Monate, B. Werner
+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,
+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) 
@@ -45,26 +60,27 @@ C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R & D)
 The following people have contributed to the development of different versions 
 of the Coq Proof assistant during the indicated time :
 
-	Bruno Barras, 	 (INRIA, 1995-2000)
+	Bruno Barras, 	 (INRIA, 1995-now)
 	Thierry Coquand (INRIA, 1985-1989)
   	Cristina Cornes, (INRIA, 1993-1996)
 	Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996)
-	David Delahaye,  (INRIA, 1997-2000)
+	David Delahaye,  (INRIA, 1997-now)
 	Daniel de Rauglaudre, (INRIA, 1996-1998)
 	Gilles Dowek, (INRIA, 1991-1994)
 	Amy Felty, (INRIA, 1993)
-	Jean-Christophe Filliâtre, (ENS Lyon, 1994-1997) (Paris 11,1997-2000)
+	Jean-Christophe Filliâtre, (ENS Lyon, 1994-1997) (Paris 11,1997-now)
 	Eduardo Giménez, (ENS Lyon, 1993-1996, INRIA, 1997-1998)
-	Hugo Herbelin, (INRIA, 1996-2000)
+	Hugo Herbelin, (INRIA, 1996-now)
 	Gérard Huet, (INRIA, 1985-1997)
+	Pierre Letouzey (LRI, 2000-now)
 	Pascal Manoury, (INRIA, 1993)
-	Micaela Mayero (INRIA, 1997-2000)
+	Micaela Mayero (INRIA, 1997-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)
   	Christine Paulin-Mohring, (INRIA, 1985-1989) (ENS Lyon, 1989-1997) 
-				  (Paris 11, 1997-2001)
+				  (Paris 11, 1997-now)
 	Amokrane Saïbi, (INRIA, 1993-1998)
 	Benjamin Werner, (INRIA, 1989-1994)