Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 52 insertions, 51 deletions

diff --git a/CREDITS b/CREDITS
index 90dbd0b2..53bd9e93 100644
--- a/CREDITS
+++ b/CREDITS
@@ -1,12 +1,14 @@
 The "Coq proof assistant" was jointly developed by 
 	
-- INRIA Formel, Coq, LogiCal, ProVal, TypiCal projects (since 1985), 
+- INRIA Formel, Coq, LogiCal, ProVal, TypiCal, Marelle, pi.r2 projects
+  (starting 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.
+  associated to CNRS and university Paris Sud (since Sep. 1997),
+- Laboratoire d'Informatique de l'Ecole Polytechnique (LIX)
+  associated to CNRS and Ecole Polytechnique (since Jan. 2003).
+- Laboratoire PPS associated to CNRS and university Paris 7 (since Jan. 2009).
 
 All files of the "Coq proof assistant" in directories or sub-directories of
 
@@ -14,7 +16,7 @@ All files of the "Coq proof assistant" in directories or sub-directories of
   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-2008,
+Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2010,
 The Coq development team, CNRS, INRIA and Université Paris Sud.
 
 Files from the directory doc are distributed as indicated in file doc/LICENCE.
@@ -23,51 +25,48 @@ The following directories contain independent contributions supported
 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
+plugins/cc
   developed by Pierre Corbineau (ENS Cachan, 2001, LRI, 2001-2005, Radboud
   University at Nijmegen, 2005-2008)
-contrib/correctness
+plugins/correctness
   developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
-contrib/dp
+plugins/dp
   developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre
   (LRI, 2005-2008)
-contrib/extraction
-  developed by Pierre Letouzey (LRI, 2000-2004, PPS-Paris7, 2005-now)
-contrib/field
+plugins/extraction
+  developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now)
+plugins/field
   developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
-contrib/firstorder 
+plugins/firstorder 
   developed by Pierre Corbineau (LRI, 2003-2008)
-contrib/fourier
+plugins/fourier
   developed by Loïc Pottier (INRIA-Lemme, 2001)
-contrib/funind
+plugins/funind
   developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2008),
   Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008) 
   and Yves Bertot (INRIA-Marelle, 2005-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-2006);
-  extended by Lionel Mamane as part of the TeXMacs project (Radboud university
-  at Nijmegen, 2007-2008)
-contrib/omega
+plugins/omega
   developed by Pierre Crégut (France Telecom R&D, 1996)
-contrib/ring
+plugins/nsatz
+  developed by Loïc Pottier (INRIA-Marelle, 2009)
+plugins/ring
   developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick 
   Loiseleur (LRI, 1997-1999)
-contrib/romega
+plugins/romega
   developed by Pierre Crégut (France Telecom R&D, 2001-2004)
-contrib/rtauto
+plugins/rtauto
   developed by Pierre Corbineau (LRI, 2005)
-contrib/setoid_ring
+plugins/setoid_ring
   developed by Benjamin Grégoire (INRIA-Everest, 2005-2006), 
   Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006) 
   and Bruno Barras (INRIA LogiCal, 2005-2006),
-contrib/subtac
+plugins/subtac
   developed by Matthieu Sozeau (LRI, 2005-2008)
-contrib/xml
+plugins/xml
   developed by Claudio Sacerdoti (Univ. Bologna, 2000-2005) 
   as part of the HELM and MoWGLI projects; extension by Cezary Kaliszyk as
   part of the ProofWeb project (Radbout University at Nijmegen, 2008)
-contrib/micromega
+plugins/micromega
   developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some 
   extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and 
   interface to the csdp solver uses code from John Harrison (University
@@ -76,40 +75,40 @@ parsing/search.ml
   mainly developed by Yves Bertot (INRIA-Lemme, 2000-2004)
 theories/ZArith
   started by Pierre Crégut (France Telecom R&D, 1996)
-theories/IntMap
-  developed by Jean Goubault-Larrecq (Dyade, 1998)
-theories/Numbers/Cyclic
-  developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry
-  (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and
-  Pierre Letouzey (PPS-Paris 7, 2008)
 theories/Strings
   developed by Laurent Théry (INRIA-Lemme, 2003)
+theories/Numbers/Cyclic
+  developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and Pierre Letouzey (PPS, 2008)
 ide/utils
   some files come from Maxence Guesdon's Cameleon tool 
 
-Many discussions within the Démons team at LRI, and the
-LogiCal/TypiCal projects influenced significantly the design of
-components of Coq, especially with
+Many discussions within the INRIA teams and labs taking part to the
+development influenced the design of Coq especially with
 
-  F. Blanqui, J. Courant, P. Courtieu, J. Duprat, S. Glondu, J. Goubault,
-  A. Mahboubi, C. Marché, A. Miquel, B. Monate, P.-Y. Strub, B. Werner.
+  C. Auger, Y. Bertot, F. Blanqui, J. Courant, P. Courtieu, J. Duprat,
+  S. Glondu, J. Goubault, J.-P. Jouannaud, S. Lescuyer, A. Mahboubi,
+  C. Marché, A. Miquel, B. Monate, L. Pottier, Y. Régis-Gianas,
+  P.-Y. Strub, L. Théry, B. Werner
 
-Intensive users suggested improvements of the system : 
+The development of Coq also significantly benefited from feedback,
+suggestions or short contributions from:
 
-  Y. Bertot, L. Pottier, L. Théry (INRIA-Lemme/Marelle projects),
   C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D),
   P. Castéran (University Bordeaux 1),
-  The Foundations Group (Radboud University, Nijmegen, The Netherlands),
+  the Foundations Group (Radboud University, Nijmegen, The Netherlands),
   Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis),
-  G. Gonthier (INRIA-MSR joint lab), A. Charguéraud (INRIA-Gallium project).
+  F. Garillot, G. Gonthier (INRIA-MSR joint lab),
+  INRIA-Gallium project, 
+  the CS dept at Yale, the CIS dept at U. Penn, 
+  the CSE dept at Harvard, the CS dept at Princeton
 
 The following people have contributed to the development of different versions 
-of the Coq Proof assistant during the indicated time :
+of the Coq Proof assistant during the indicated time:
 
   Bruno Barras (INRIA, 1995-now)
   Jacek Chrzaszcz (LRI, 1998-2003)
   Thierry Coquand (INRIA, 1985-1989)
-  Pierre Corbineau (LRI, 2003-now)
+  Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-now)
   Cristina Cornes (INRIA, 1993-1996)
   Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996)
   David Delahaye (INRIA, 1997-2002)
@@ -122,15 +121,15 @@ of the Coq Proof assistant during the indicated time :
   Benjamin Grégoire (INRIA, 2003-now)
   Hugo Herbelin (INRIA, 1996-now)
   Gérard Huet (INRIA, 1985-1997)
-  Pierre Letouzey (LRI, 2000-2004 & PPS-Paris 7, 2005-now)
+  Pierre Letouzey (LRI, 2000-2004 & PPS, 2005-now)
   Evgeny Makarov (INRIA, 2007)
   Pascal Manoury (INRIA, 1993)
   Micaela Mayero (INRIA, 1997-2002)
-  Claude Marché (INRIA 2003-2004 & LRI, 2004-now)
+  Claude Marché (INRIA 2003-2004 & LRI, 2004)
   Benjamin Monate (LRI, 2003)
   César Muñoz (INRIA, 1994-1995)
   Chetan Murthy (INRIA, 1992-1994)
-  Julien Narboux (INRIA, 2005-2006)
+  Julien Narboux (INRIA, 2005-2006, Strasbourg, 2007-now)
   Jean-Marc Notin (CNRS, 2006-now)
   Catherine Parent-Vigouroux (ENS Lyon, 1992-1995)
   Patrick Loiseleur (Paris Sud, 1997-1999)
@@ -146,12 +145,14 @@ of the Coq Proof assistant during the indicated time :
   Benjamin Werner (INRIA, 1989-1994)
 
 ***************************************************************************
-INRIA refers to :
+INRIA refers to:
   Institut National de la Recherche en Informatique et Automatique
-CNRS refers to :
+CNRS refers to:
   Centre National de la Recherche Scientifique
-LRI refers to : Laboratoire de Recherche en Informatique, UMR 8623 
+LRI refers to: Laboratoire de Recherche en Informatique, UMR 8623
   CNRS and Université Paris-Sud
-ENS Lyon refers to :
+ENS Lyon refers to:
   Ecole Normale Supérieure de Lyon
+PPS refers to: Laboratoire Preuve, Programmation, Système, UMR 7126,
+  CNRS and Université Paris 7
 ****************************************************************************