Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 102 insertions, 81 deletions

diff --git a/CREDITS b/CREDITS
index 12cd8e65..0bc6ee56 100644
--- a/CREDITS
+++ b/CREDITS
@@ -1,115 +1,136 @@
-
-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.
+The "Coq proof assistant" was jointly developed by 
+	
+- INRIA Formel, Coq, LogiCal, ProVal 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
+
+  config dev ide interp kernel lib library parsing pretyping proofs
+  scripts states 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
+Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2006,
+The Coq development team, CNRS, INRIA and Université Paris Sud.
 
+Files from the directory doc are distributed as indicated in file doc/LICENCE.
 
 The following directories contain independent contributions supported 
-by the Coq development team :
+by the Coq development team. All of them are released under the terms of
+the GNU Lesser General Public License Version 2.1.
+
 contrib/cc
-	developed by Pierre Corbineau (ENS Cachan, 2001)
+  developed by Pierre Corbineau (ENS Cachan, 2001 and LRI, 2001-2005)
 contrib/correctness
-	developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
+  developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
+contrib/dp
+  developed by Nicolas Ayache and Jean-Christophe Filliâtre (LRI, 2005-2006)
 contrib/extraction
-	developed by Pierre Letouzey (LRI, 2000-2004)
+  developed by Pierre Letouzey (LRI, 2000-2006)
 contrib/field
-	developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
+  developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
 contrib/first-order 
-	developed by Pierre Corbineau (LRI, 2003-2004)
+  developed by Pierre Corbineau (LRI, 2003-2005)
 contrib/fourier
-	developed by Loïc Pottier (INRIA-Lemme, 2001)
+  developed by Loïc Pottier (INRIA-Lemme, 2001)
 contrib/funind
-	developed by Pierre Courtieu (INRIA-Lemme, 2003-2004)
+  developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2006)
+  and Julien Forest, Benjamin Grégoire and Gilles Barthe (INRIA-Everest, 2006)
 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"
+  developed by Yves Bertot with contributions from Loïc Pottier and
+  Laurence Rideau as part of the Pcoq project (INRIA-Lemme, 1997-2006)
 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)
+  developed by Pierre Crégut (France Telecom R&D, 1996)
+contrib/recdef
+  developed by Yves Bertot (INRIA-Marelle, 2005)
 contrib/ring
-	developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick 
-	Loiseleur (LRI, 1997-1999)
+  developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick 
+  Loiseleur (LRI, 1997-1999)
+contrib/romega
+  developed by Pierre Crégut (France Telecom R&D, 2001-2004)
+contrib/rtauto
+  developed by Pierre Corbineau (LRI, 2005)
+contrib/setoid_ring
+  developed by Benjamin Grégoire, Assia Mahboubi (INRIA-Marelle, 2005-2006)
+  and Bruno Barras (INRIA LogiCal, 2005-2006)
+contrib/subtac
+  developed by Matthieu Sozeau (LRI, 2005-2006)
 contrib/xml
-	developed by Claudio Sacerdoti (Univ. Bologna, 2000-2004) 
-	as part of the HELM and MoWGLI project
+  developed by Claudio Sacerdoti (Univ. Bologna, 2000-2005) 
+  as part of the HELM and MoWGLI projects
 
 parsing/search.ml
-	developed by Yves Bertot (INRIA-Lemme, 2000-2004)
+  mainly 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"
+  started by Pierre Crégut (France Telecom R&D, 1996)
+theories/IntMap
+  developed by Jean Goubault-Larrecq (Dyade, 1998)
+theories/Strings
+  developed by Laurent Théry (INRIA-Lemme, 2003)
+ide/utils
+  some files come from Maxence Guesdon's Cameleon tool 
 
-Many discussions within the Démons team and the LogiCal project
+Many discussions within the Démons team at LRI 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
+
+  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)
+
+  Y. Bertot, L. Pottier, L. Théry (INRIA-Lemme projects),
+  C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D),
+  P. Castéran (University Bordeaux 1),
+  The Foundations Group (Radbout University, Nijmegen, The Netherlands),
+  Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis).
 
 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)
-
+  Bruno Barras (INRIA, 1995-now)
+  Jacek Chrzaszcz (LRI, 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, LRI, 1997-now)
+  Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998)
+  Benjamin Grégoire (INRIA, 2003-now)
+  Hugo Herbelin (INRIA, 1996-now)
+  Gérard Huet (INRIA, 1985-1997)
+  Pierre Letouzey (LRI, 2000-2005 & PPS-Paris 7, 2005-now)
+  Pascal Manoury (INRIA, 1993)
+  Micaela Mayero (INRIA, 1997-2002)
+  Claude Marché (INRIA 2003-2004 & LRI, 2004-now)
+  Benjamin Monate (LRI, 2003)
+  César Muñoz (INRIA, 1994-1995)
+  Chetan Murthy (INRIA, 1992-1994)
+  Julien Narboux (INRIA, 2005-2006)
+  Jean-Marc Notin (CNRS, 2006)
+  Catherine Parent-Vigouroux (ENS Lyon, 1992-1995)
+  Patrick Loiseleur (Paris Sud, 1997-1999)
+  Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997, 
+                            LRI, 1997-now)
+  Clément Renard (INRIA, 2001-2004)
+  Claudio Sacerdoti Coen (INRIA, 2004-2005)
+  Amokrane Saïbi (INRIA, 1993-1998)
+  Benjamin Werner (INRIA, 1989-1994)
 
 ***************************************************************************
 INRIA refers to :
-	Institut National de la Recherche en Informatique et Automatique
+  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
+  Centre National de la Recherche Scientifique
+LRI refers to : Laboratoire de Recherche en Informatique, UMR 8623 
+  CNRS and Université Paris-Sud
 ENS Lyon refers to :
-	Ecole Normale Supérieure de Lyon
+  Ecole Normale Supérieure de Lyon
 ****************************************************************************