Update of credits files

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

2 files changed, 115 insertions, 35 deletions

diff --git a/CREDITS b/CREDITS
index 3587eec59..68009d390 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.
@@ -32,7 +34,7 @@ plugins/dp
   developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre
   (LRI, 2005-2008)
 plugins/extraction
-  developed by Pierre Letouzey (LRI, 2000-2004, PPS-Paris7, 2005-now)
+  developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now)
 plugins/field
   developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
 plugins/firstorder 
@@ -43,13 +45,10 @@ 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)
-plugins/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)
 plugins/omega
   developed by Pierre Crégut (France Telecom R&D, 1996)
+plugins/groebner
+  developed by Loïc Pottier (INRIA-Marelle, 2009)
 plugins/ring
   developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick 
   Loiseleur (LRI, 1997-1999)
@@ -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
 ****************************************************************************
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 736627122..8ec3c2e7f 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -691,6 +691,83 @@ Palaiseau, June 2008\\
 Hugo Herbelin\\
 \end{flushright}
 
+\section*{Credits: version 8.3}
+
+{\Coq} version 8.3 is before all a transition version with refinements
+or extensions of the existing features and libraries and a new tactic
+{\tt gb} based on Hilbert's Nullstellensatz for deciding systems of
+equations over rings.
+
+With respect to libraries, the main evolutions are due to Pierre
+Letouzey with a rewriting of the library of finite sets {\tt FSets}
+and a new round of evolutions in the modular development of arithmetic
+(library {\tt Numbers}). The reason for making {\tt FSets} evolve is
+that the computational and logical contents were quite intertwined in
+the original implementation, leading in some cases to longer
+computations than expected and this problem is solved in the new {\tt
+  MSets} implementation. As for the modular arithmetic library, it was
+only dealing with the basic arithmetic operators in the former version
+and its current extension adds the standard theory of the division,
+min and max functions, all made available for free to any
+implementation of $\mathbb{N}$, $\mathbb{Z}$ or
+$\mathbb{Z}/n\mathbb{Z}$. 
+
+The main other evolutions of the library are due to Hugo Herbelin who
+made a revision of the sorting library (includingh a certified
+merge-sort) and to Guillaume Melquiond who slightly revised and
+cleaned up the library of reals.
+
+The module system evolved significantly. Besides the resolution of
+some efficiency issues and a more flexible construction of module
+types, Élie Soubiran brought a new model of name equivalence, the
+$\Delta$-equivalence, which respects as much as possible the names
+given by the users. He also designed with Pierre Letouzey a new
+convenient operator \verb!<+! for nesting functor application, what
+provides a light notation for inheriting the properties of cascading
+modules.
+
+The new tactic {\tt gb} is due to Loïc Pottier. It works by computing
+Gr\"obner bases what explains its name. Regarding the existing
+tactics, various improvements have been done by Matthieu Sozeau, Hugo
+Herbelin and Pierre Letouzey.
+
+Matthieu Sozeau extended and refined the type classes and {\tt
+  Program} features (the {\sc Russell} language). Pierre Letouzey
+maintained and improved the extraction mechanism.  Bruno Barras and
+\'Elie Soubiran maintained the Coq checker, Julien Forest maintained
+the {\tt Function} mechanism for reasoning over recursively defined
+functions. Matthieu Sozeau, Hugo Herbelin and Jean-Marc Notin
+maintained {\tt coqdoc}. Frédéric Besson maintained the {\sc
+  Micromega} plateform for deciding systems of inequalities. Pierre
+Courtieu maintained the support for the Proof General Emacs
+interface. Claude Marché maintained the plugin for calling external
+provers ({\tt dp}). Yves Bertot made some improvements to the
+libraries of lists and integers. Matthias Puech improved the search
+functions. Guillaume Melquiond usefully contributed here and
+there. Yann Régis-Gianas grounded the support for Unicode on a more
+standard and more robust basis.
+
+Though invisible from outside, Arnaud Spiwack improved the general
+process of management of existential variables. Pierre Letouzey and
+Stéphane Glondu improved the compilation scheme of the Coq archive.
+Vincent Gross provided support to CoqIDE. Jean-Marc Notin provided
+support for benchmarking and archiving.
+
+Many users helped by reporting problems, providing patches, suggesting
+improvements or making useful comments, either on the bug tracker or
+on the Coq-club mailing list. This includes but not exhaustively
+Cédric Auger, Arthur Charguéraud, François Garillot, Georges Gonthier,
+Robin Green, Stéphane Lescuyer, Eelis van der Weegen,~...
+
+Though not directly related to the implementation, special thanks are
+going to Yves Bertot, Pierre Castéran, Adam Chlipala, and Benjamin
+Pierce for the excellent teaching materials they provided.
+
+\begin{flushright}
+Paris, April 2010\\
+Hugo Herbelin\\
+\end{flushright}
+
 %new Makefile
 
 %\newpage
@@ -698,6 +775,8 @@ Hugo Herbelin\\
 % Integration of ZArith lemmas from Sophia and Nijmegen.
 
 
+% $Id$ 
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"